# Theory Green

```theory Green
imports Paths Derivs Integrals General_Utils
begin

lemma frontier_Un_subset_Un_frontier:
"frontier (s ∪ t) ⊆ (frontier s) ∪ (frontier t)"

definition has_partial_derivative:: "(('a::euclidean_space) ⇒ 'b::euclidean_space) ⇒ 'a ⇒ ('a ⇒ 'b) ⇒ ('a) ⇒ bool" where
"has_partial_derivative F base_vec F' a
≡ ((λx::'a::euclidean_space. F( (a - ((a ∙ base_vec) *⇩R base_vec)) + (x ∙ base_vec) *⇩R base_vec ))
has_derivative F') (at a)"

definition has_partial_vector_derivative:: "(('a::euclidean_space) ⇒ 'b::euclidean_space) ⇒ 'a ⇒ ( 'b) ⇒ ('a) ⇒ bool" where
"has_partial_vector_derivative F base_vec F' a
≡ ((λx. F( (a - ((a ∙ base_vec) *⇩R base_vec)) + x *⇩R base_vec ))
has_vector_derivative F') (at (a ∙ base_vec))"

definition partially_vector_differentiable where
"partially_vector_differentiable F base_vec p ≡ (∃F'. has_partial_vector_derivative F base_vec F' p)"

definition partial_vector_derivative:: "(('a::euclidean_space) ⇒ 'b::euclidean_space) ⇒ 'a ⇒ 'a ⇒ 'b" where
"partial_vector_derivative F base_vec a
≡ (vector_derivative (λx. F( (a - ((a ∙ base_vec) *⇩R base_vec)) + x *⇩R base_vec)) (at (a ∙ base_vec)))"

lemma partial_vector_derivative_works:
assumes "partially_vector_differentiable F base_vec a"
shows "has_partial_vector_derivative F base_vec (partial_vector_derivative F base_vec a) a"
proof -
obtain F' where F'_prop: "((λx. F( (a - ((a ∙ base_vec) *⇩R base_vec)) + x *⇩R base_vec ))
has_vector_derivative F') (at (a ∙ base_vec))"
using assms partially_vector_differentiable_def has_partial_vector_derivative_def
by blast
show ?thesis
using Derivative.differentiableI_vector[OF F'_prop]
has_partial_vector_derivative_def[symmetric])
qed

lemma fundamental_theorem_of_calculus_partial_vector:
fixes a b:: "real" and
F:: "('a::euclidean_space ⇒ 'b::euclidean_space)" and
i:: "'a" and
j:: "'b" and
F_j_i:: "('a::euclidean_space ⇒ real)"
assumes a_leq_b: "a ≤ b" and
Base_vecs: "i ∈ Basis" "j ∈ Basis" and
no_i_component: "c ∙ i = 0 " and
has_partial_deriv: "∀p ∈ D. has_partial_vector_derivative (λx. (F x) ∙ j) i (F_j_i p) p" and
domain_subset_of_D: "{x *⇩R i + c |x. a ≤ x ∧ x ≤ b} ⊆ D"
shows "((λx. F_j_i( x *⇩R i + c)) has_integral
F(b *⇩R i + c) ∙ j - F(a *⇩R i + c) ∙ j) (cbox a b)"
proof -
let ?domain = "{v. ∃x. a ≤ x ∧ x ≤ b ∧ v = x *⇩R i + c}"
have "∀x∈ ?domain.  has_partial_vector_derivative (λx. (F x) ∙ j) i (F_j_i x) x"
using has_partial_deriv domain_subset_of_D
by auto
then have "∀x∈ (cbox a b).  ((λx. F(x *⇩R i + c) ∙ j) has_vector_derivative (F_j_i( x *⇩R i + c))) (at x)"
fix x::real
assume range_of_x: "a ≤ x" "x ≤ b"
assume ass2: "∀x. (∃z≥a. z ≤ b ∧ x = z *⇩R i + c) ⟶
((λz. F(x - (x ∙ i) *⇩R i + z *⇩R i) ∙ j) has_vector_derivative F_j_i x) (at (x ∙ i))"
have "((λz. F((x *⇩R i + c) - ((x *⇩R i + c) ∙ i) *⇩R i + z *⇩R i) ∙ j) has_vector_derivative F_j_i (x *⇩R i + c)) (at ((x *⇩R i + c) ∙ i)) "
using range_of_x ass2 by auto
then have 0: "((λx. F( c + x *⇩R i) ∙ j) has_vector_derivative F_j_i (x *⇩R i + c)) (at x)"
by (simp add: assms(2) inner_left_distrib no_i_component)
have 1: "(λx. F(x *⇩R i + c) ∙ j) = (λx. F(c + x *⇩R i) ∙ j)"
then show "((λx. F(x *⇩R i + c) ∙ j) has_vector_derivative F_j_i (x *⇩R i + c)) (at x)"
using 0 and 1 by auto
qed
then have "∀x∈ (cbox a b).  ((λx. F(x *⇩R i + c) ∙ j) has_vector_derivative (F_j_i( x *⇩R i + c))) (at_within x (cbox a b))"
using has_vector_derivative_at_within
by blast
then show "( (λx. F_j_i( x *⇩R i + c)) has_integral
F(b *⇩R i + c) ∙ j - F(a *⇩R i + c) ∙ j) (cbox a b)"
using fundamental_theorem_of_calculus[of "a" "b" "(λx::real.  F(x *⇩R i + c) ∙ j)" "(λx::real. F_j_i( x *⇩R i + c))"] and
a_leq_b
by auto
qed

lemma fundamental_theorem_of_calculus_partial_vector_gen:
fixes k1 k2:: "real" and
F:: "('a::euclidean_space ⇒ 'b::euclidean_space)" and
i:: "'a" and
F_i:: "('a::euclidean_space ⇒ 'b)"
assumes a_leq_b: "k1 ≤ k2" and
unit_len: "i ∙ i = 1" and
no_i_component: "c ∙ i = 0 " and
has_partial_deriv: "∀p ∈ D. has_partial_vector_derivative F i (F_i p) p" and
domain_subset_of_D: "{v. ∃x. k1 ≤ x ∧ x ≤ k2 ∧ v = x *⇩R i + c} ⊆ D"
shows "( (λx. F_i( x *⇩R i + c)) has_integral
F(k2 *⇩R i + c) - F(k1 *⇩R i + c)) (cbox k1 k2)"
proof -
let ?domain = "{v. ∃x. k1 ≤ x ∧ x ≤ k2 ∧ v = x *⇩R i + c}"
have "∀x∈ ?domain.  has_partial_vector_derivative F i (F_i x) x"
using has_partial_deriv domain_subset_of_D
by auto
then have "∀x∈ (cbox k1 k2).  ((λx. F(x *⇩R i + c)) has_vector_derivative (F_i( x *⇩R i + c))) (at x)"
fix x::real
assume range_of_x: "k1 ≤ x" "x ≤ k2"
assume ass2: "∀x. (∃z≥k1. z ≤ k2 ∧ x = z *⇩R i + c) ⟶
((λz. F(x - (x ∙ i) *⇩R i + z *⇩R i)) has_vector_derivative F_i x) (at (x ∙ i))"
have "((λz. F((x *⇩R i + c) - ((x *⇩R i + c) ∙ i) *⇩R i + z *⇩R i)) has_vector_derivative F_i (x *⇩R i + c)) (at ((x *⇩R i + c) ∙ i)) "
using range_of_x ass2 by auto
then have 0: "((λx. F( c + x *⇩R i)) has_vector_derivative F_i (x *⇩R i + c)) (at x)"
by (simp add: inner_commute inner_right_distrib no_i_component unit_len)
have 1: "(λx. F(x *⇩R i + c)) = (λx. F(c + x *⇩R i))"
then show "((λx. F(x *⇩R i + c)) has_vector_derivative F_i (x *⇩R i + c)) (at x)" using 0 and 1 by auto
qed
then have "∀x∈ (cbox k1 k2).  ((λx. F(x *⇩R i + c) ) has_vector_derivative (F_i( x *⇩R i + c))) (at_within x (cbox k1 k2))"
using has_vector_derivative_at_within
by blast
then show "( (λx. F_i( x *⇩R i + c)) has_integral
F(k2 *⇩R i + c) - F(k1 *⇩R i + c)) (cbox k1 k2)"
using fundamental_theorem_of_calculus[of "k1" "k2" "(λx::real.  F(x *⇩R i + c))" "(λx::real. F_i( x *⇩R i + c))"] and
a_leq_b
by auto
qed

assumes "a < b" shows "(λx::real. a + (b - a) * x) ` {0 .. 1} = {a .. b}"
using assms
apply (auto simp: algebra_simps affine_ineq image_iff)
using less_eq_real_def apply force
apply (rule_tac x="(x-a)/(b-a)" in bexI)
apply (auto simp: field_simps)
done

assumes "a ≤ b"
shows "(λx::real. a + (b - a) * x) ` {0 .. 1} = {a .. b}"
proof (cases "a = b")
case True
then show ?thesis by force
next
case False
then show ?thesis
qed

definition analytically_valid:: "'a::euclidean_space set ⇒ ('a ⇒ 'b::{euclidean_space,times,zero_neq_one}) ⇒ 'a ⇒ bool" where
"analytically_valid s F i ≡
(∀a ∈ s. partially_vector_differentiable F i a) ∧
continuous_on s F ∧ ― ‹TODO: should we replace this with saying that ‹F› is partially diffrerentiable on ‹Dy›,›
― ‹i.e. there is a partial derivative on every dimension›
integrable lborel (λp. (partial_vector_derivative F i) p * indicator s p) ∧
(λx. integral UNIV (λy. (partial_vector_derivative F i (y *⇩R i + x *⇩R (∑ b ∈(Basis - {i}). b)))
* (indicator s (y *⇩R i + x *⇩R (∑b ∈ Basis - {i}. b)) ))) ∈ borel_measurable lborel"
(*(λx. integral UNIV (λy. ((partial_vector_derivative F i) (y, x)) * (indicator s (y, x)))) ∈ borel_measurable lborel)"*)

lemma analytically_valid_imp_part_deriv_integrable_on:
assumes "analytically_valid (s::(real*real) set) (f::(real*real)⇒ real) i"
shows "(partial_vector_derivative f i) integrable_on s"
proof -
have "integrable lborel (λp. partial_vector_derivative f i p * indicator s p)"
using assms
then have "integrable lborel (λp::(real*real). if p ∈ s then partial_vector_derivative f i p else 0)"
using indic_ident[of "partial_vector_derivative f i"]
then have "(λx. if x ∈ s then partial_vector_derivative f i x else 0) integrable_on UNIV"
using Equivalence_Lebesgue_Henstock_Integration.integrable_on_lborel
by auto
then show "(partial_vector_derivative f i) integrable_on s"
using integrable_restrict_UNIV
by auto
qed

(*******************************************************************************)

definition typeII_twoCube :: "((real * real) ⇒ (real * real)) ⇒ bool" where
"typeII_twoCube twoC
≡ ∃a b g1 g2. a < b ∧ (∀x ∈ {a..b}. g2 x ≤ g1 x) ∧
twoC = (λ(y, x). ((1 - y) * (g2 ((1-x)*a + x*b)) + y * (g1 ((1-x)*a + x*b)),
(1-x)*a + x*b)) ∧
g1 piecewise_C1_differentiable_on {a .. b} ∧
g2 piecewise_C1_differentiable_on {a .. b}"

abbreviation unit_cube where "unit_cube ≡ cbox (0,0) (1::real,1::real)"

definition cubeImage:: "two_cube ⇒ ((real*real) set)" where
"cubeImage twoC ≡ (twoC ` unit_cube)"

lemma typeII_twoCubeImg:
assumes "typeII_twoCube twoC"
shows "∃a b g1 g2. a < b ∧ (∀x ∈ {a .. b}. g2 x ≤ g1 x) ∧
cubeImage twoC = {(y,x). x ∈ {a..b} ∧ y ∈ {g2 x .. g1 x}}
∧ twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b))
∧ g1 piecewise_C1_differentiable_on {a .. b} ∧ g2 piecewise_C1_differentiable_on {a .. b} "
using assms
proof (simp add: typeII_twoCube_def cubeImage_def image_def)
assume " ∃a b. a < b ∧ (∃g1 g2. (∀x∈{a..b}. g2 x ≤ g1 x) ∧
twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b)) ∧
g1 piecewise_C1_differentiable_on {a..b} ∧ g2 piecewise_C1_differentiable_on {a..b})"
then obtain a b g1 g2 where
twoCisTypeII: "a < b"
"(∀x∈{a..b}. g2 x ≤ g1 x)"
"twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
by auto
have ab1: "a - x * a + x * b ≤ b" if a1: "0 ≤ x" "x ≤ 1" for x
using that apply (simp add: algebra_simps)
by (metis affine_ineq less_eq_real_def mult.commute twoCisTypeII(1))
have ex: "∃z∈Green.unit_cube.
(d, c) =
(case z of
(y, x) ⇒
(g2 (a - x * a + x * b) - y * g2 (a - x * a + x * b) + y * g1 (a - x * a + x * b),
a - x * a + x * b))"
if c_bounds: "a ≤ c" "c ≤ b" and d_bounds: "g2 c ≤ d" "d ≤ g1 c" for c d
proof -
have b_minus_a_nzero: "b - a ≠ 0" using twoCisTypeII(1) by auto
have x_witness: "∃k1. c = (1 - k1)*a + k1 * b ∧ 0 ≤ k1 ∧ k1 ≤ 1"
apply (rule_tac x="(c - a)/(b - a)" in exI)
using c_bounds ‹a < b› apply (simp add: divide_simps algebra_simps)
using sum_sqs_eq by blast
have y_witness: "∃k2. d = (1 - k2)*(g2 c) + k2 * (g1 c) ∧ 0 ≤ k2 ∧ k2 ≤ 1"
proof (cases "g1 c - g2 c = 0")
case True
with d_bounds show ?thesis by (fastforce simp add: algebra_simps)
next
case False
let ?k2 = "(d - g2 c)/(g1 c - g2 c)"
have k2_in_bounds: "0 ≤ ?k2 ∧ ?k2 ≤ 1"
using twoCisTypeII(2) c_bounds d_bounds False by simp
have "d = (1 - ?k2) * g2 c + ?k2 * g1 c"
using False sum_sqs_eq by (fastforce simp add: divide_simps algebra_simps)
with k2_in_bounds show ?thesis
by fastforce
qed
show "∃x∈unit_cube. (d, c) = (case x of (y, x) ⇒ (g2 (a - x * a + x * b) - y * g2 (a - x * a + x * b) + y * g1 (a - x * a + x * b), a - x * a + x * b))"
using x_witness y_witness by (force simp add: left_diff_distrib)
qed
have "{y. ∃x∈unit_cube. y = twoC x} = {(y, x). a ≤ x ∧ x ≤ b ∧ g2 x ≤ y ∧ y ≤ g1 x}"
apply (auto simp add: twoCisTypeII ab1 left_diff_distrib ex)
using order.order_iff_strict twoCisTypeII(1) apply fastforce
apply (smt affine_ineq atLeastAtMost_iff mult_left_mono twoCisTypeII)+
done
then show "∃a b. a < b ∧ (∃g1 g2. (∀x∈{a..b}. g2 x ≤ g1 x) ∧
{y. ∃x∈unit_cube. y = twoC x} = {(y, x). a ≤ x ∧ x ≤ b ∧ g2 x ≤ y ∧ y ≤ g1 x} ∧
twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b)) ∧
g1 piecewise_C1_differentiable_on {a..b} ∧ g2 piecewise_C1_differentiable_on {a..b})"
using twoCisTypeII by blast
qed

definition horizontal_boundary :: "two_cube ⇒ one_chain" where
"horizontal_boundary twoC ≡ {(1, (λx. twoC(x,0))), (-1, (λx. twoC(x,1)))}"

definition vertical_boundary :: "two_cube ⇒ one_chain" where
"vertical_boundary twoC ≡ {(-1, (λy. twoC(0,y))), (1, (λy. twoC(1,y)))}"

definition boundary :: "two_cube ⇒ one_chain" where
"boundary twoC ≡ horizontal_boundary twoC ∪ vertical_boundary twoC"

definition valid_two_cube where
"valid_two_cube twoC ≡ card (boundary twoC) = 4"

definition two_chain_integral:: "two_chain ⇒ ((real*real)⇒(real)) ⇒ real" where
"two_chain_integral twoChain F ≡ ∑C∈twoChain. (integral (cubeImage C) F)"

definition valid_two_chain where
"valid_two_chain twoChain ≡ (∀twoCube ∈ twoChain. valid_two_cube twoCube) ∧ pairwise (λc1 c2. ((boundary c1) ∩ (boundary c2)) = {}) twoChain ∧ inj_on cubeImage twoChain"

definition two_chain_boundary:: "two_chain ⇒ one_chain" where
"two_chain_boundary twoChain == ⋃(boundary ` twoChain)"

definition gen_division where
"gen_division s S ≡ (finite S ∧ (⋃S = s) ∧ pairwise (λX Y. negligible (X ∩ Y)) S)"

definition two_chain_horizontal_boundary:: "two_chain ⇒ one_chain" where
"two_chain_horizontal_boundary twoChain  ≡ ⋃(horizontal_boundary ` twoChain)"

definition two_chain_vertical_boundary:: "two_chain ⇒ one_chain" where
"two_chain_vertical_boundary twoChain  ≡ ⋃(vertical_boundary ` twoChain)"

definition only_horizontal_division where
"only_horizontal_division one_chain two_chain
≡ ∃ℋ 𝒱. finite ℋ ∧ finite 𝒱 ∧
(∀(k,γ) ∈ ℋ.
(∃(k', γ') ∈ two_chain_horizontal_boundary two_chain.
(∃a ∈ {0..1}. ∃b ∈ {0..1}. a ≤ b ∧ subpath a b γ' = γ))) ∧
(common_sudiv_exists (two_chain_vertical_boundary two_chain) 𝒱
∨ common_reparam_exists 𝒱 (two_chain_vertical_boundary two_chain)) ∧
boundary_chain 𝒱 ∧
one_chain = ℋ ∪ 𝒱 ∧ (∀(k,γ)∈𝒱. valid_path γ)"

lemma sum_zero_set:
assumes "∀x ∈ s. f x = 0" "finite s" "finite t"
shows "sum f (s ∪ t) = sum f t"
using assms
by (simp add: IntE sum.union_inter_neutral sup_commute)

abbreviation "valid_typeII_division s twoChain ≡ ((∀twoCube ∈ twoChain. typeII_twoCube twoCube) ∧
(gen_division s (cubeImage ` twoChain)) ∧
(valid_two_chain twoChain))"

lemma two_chain_vertical_boundary_is_boundary_chain:
shows "boundary_chain (two_chain_vertical_boundary twoChain)"

lemma two_chain_horizontal_boundary_is_boundary_chain:
shows "boundary_chain (two_chain_horizontal_boundary twoChain)"

definition typeI_twoCube :: "two_cube ⇒ bool" where
"typeI_twoCube (twoC::two_cube)
≡ ∃a b g1 g2. a < b ∧ (∀x ∈ {a..b}. g2 x ≤ g1 x) ∧
twoC = (λ(x,y). ((1-x)*a + x*b,
(1 - y) * (g2 ((1-x)*a + x*b)) + y * (g1 ((1-x)*a + x*b)))) ∧
g1 piecewise_C1_differentiable_on {a..b} ∧
g2 piecewise_C1_differentiable_on {a..b}"

lemma typeI_twoCubeImg:
assumes "typeI_twoCube twoC"
shows "∃a b g1 g2. a < b ∧ (∀x ∈ {a .. b}. g2 x ≤ g1 x) ∧
cubeImage twoC = {(x,y). x ∈ {a..b} ∧ y ∈ {g2 x .. g1 x}} ∧
twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b))) ∧
g1 piecewise_C1_differentiable_on {a .. b} ∧ g2 piecewise_C1_differentiable_on {a .. b} "
proof -
have "∃a b. a < b ∧
(∃g1 g2. (∀x∈{a..b}. g2 x ≤ g1 x) ∧
twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b)))∧
g1 piecewise_C1_differentiable_on {a .. b} ∧ g2 piecewise_C1_differentiable_on {a .. b})"
using assms by (simp add: typeI_twoCube_def)
then obtain a b g1 g2 where
twoCisTypeI: "a < b"
"(∀x∈{a..b}. g2 x ≤ g1 x)"
"twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b)))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
by auto
have ex: "∃z∈Green.unit_cube.
(c, d) =
(case z of
(x, y) ⇒
(a - x * a + x * b,
g2 (a - x * a + x * b) - y * g2 (a - x * a + x * b) + y * g1 (a - x * a + x * b)))"
if c_bounds: "a ≤ c" "c ≤ b" and  d_bounds: "g2 c ≤ d" "d ≤ g1 c" for c d
proof -
have x_witness: "∃k1. c = (1 - k1)*a + k1 * b ∧ 0 ≤ k1 ∧ k1 ≤ 1"
proof -
let ?k1 = "(c - a)/(b - a)"
have k1_in_bounds: "0 ≤ (c - a)/(b - a) ∧ (c - a)/(b - a) ≤ 1"
using twoCisTypeI(1) c_bounds by simp
have "c = (1 - ?k1)*a + ?k1 * b"
using twoCisTypeI(1) sum_sqs_eq
by (auto simp add: divide_simps algebra_simps)
then show ?thesis
using twoCisTypeI k1_in_bounds by fastforce
qed
have y_witness: "∃k2. d = (1 - k2)*(g2 c) + k2 * (g1 c) ∧ 0 ≤ k2 ∧ k2 ≤ 1"
proof (cases "g1 c - g2 c = 0")
case True
with d_bounds show ?thesis
by force
next
case False
let ?k2 = "(d - g2 c)/(g1 c - g2 c)"
have k2_in_bounds: "0 ≤ ?k2 ∧ ?k2 ≤ 1" using twoCisTypeI(2) c_bounds d_bounds False by simp
have "d = (1 - ?k2) * g2 c + ?k2 * g1 c"
using False apply (simp add: divide_simps algebra_simps)
using sum_sqs_eq by fastforce
then show ?thesis using k2_in_bounds by fastforce
qed
show "∃x∈unit_cube. (c, d) =
(case x of (x, y) ⇒ (a - x * a + x * b, g2 (a - x * a + x * b) - y * g2 (a - x * a + x * b) + y * g1 (a - x * a + x * b)))"
using x_witness y_witness by (force simp add: left_diff_distrib)
qed
have "{y. ∃x∈unit_cube. y = twoC x} = {(x, y). a ≤ x ∧ x ≤ b ∧ g2 x ≤ y ∧ y ≤ g1 x}"
apply (auto simp add: twoCisTypeI left_diff_distrib ex)
using less_eq_real_def twoCisTypeI(1) apply auto[1]
apply (smt affine_ineq twoCisTypeI)
apply (smt affine_ineq atLeastAtMost_iff mult_left_mono twoCisTypeI)+
done
then show ?thesis
unfolding cubeImage_def image_def using twoCisTypeI by auto
qed

lemma typeI_cube_explicit_spec:
assumes "typeI_twoCube twoC"
shows "∃a b g1 g2. a < b ∧ (∀x ∈ {a .. b}. g2 x ≤ g1 x) ∧
cubeImage twoC = {(x,y). x ∈ {a..b} ∧ y ∈ {g2 x .. g1 x}}
∧ twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b)))
∧ g1 piecewise_C1_differentiable_on {a .. b} ∧ g2 piecewise_C1_differentiable_on {a .. b}
∧ (λx. twoC(x, 0)) = (λx. (a + (b - a) * x, g2 (a + (b - a) * x)))
∧ (λy. twoC(1, y)) = (λx. (b, g2 b + x *⇩R (g1 b - g2 b)))
∧ (λx. twoC(x, 1)) = (λx. (a + (b - a) * x, g1 (a + (b - a) * x)))
∧ (λy. twoC(0, y)) = (λx. (a, g2 a + x *⇩R (g1 a - g2 a)))"
proof -
let ?bottom_edge = "(λx. twoC(x, 0))"
let ?right_edge = "(λy. twoC(1, y))"
let ?top_edge = "(λx. twoC(x, 1))"
let ?left_edge = "(λy. twoC(0, y))"
obtain a b g1 g2 where
twoCisTypeI: "a < b"
"(∀x ∈ cbox a b. g2 x ≤ g1 x)"
"cubeImage twoC = {(x,y). x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}"
"twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b)))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
using assms and typeI_twoCubeImg[of"twoC"] by auto
have bottom_edge_explicit: "?bottom_edge = (λx. (a + (b - a) * x, g2 (a + (b - a) * x)))"
have right_edge_explicit: "?right_edge = (λx. (b, g2 b + x *⇩R (g1 b - g2 b)))"
have top_edge_explicit: "?top_edge = (λx. (a + (b - a) * x, g1 (a + (b - a) * x)))"
have left_edge_explicit: "?left_edge = (λx. (a, g2 a + x *⇩R (g1 a - g2 a)))"
show ?thesis
using bottom_edge_explicit right_edge_explicit top_edge_explicit left_edge_explicit twoCisTypeI
by auto
qed

lemma typeI_twoCube_smooth_edges:
assumes "typeI_twoCube twoC"
"(k,γ) ∈ boundary twoC"
shows "γ piecewise_C1_differentiable_on {0..1}"
proof -
let ?bottom_edge = "(λx. twoC(x, 0))"
let ?right_edge = "(λy. twoC(1, y))"
let ?top_edge = "(λx. twoC(x, 1))"
let ?left_edge = "(λy. twoC(0, y))"
obtain a b g1 g2 where
twoCisTypeI: "a < b"
"(∀x ∈ cbox a b. g2 x ≤ g1 x)"
"cubeImage twoC = {(x,y). x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}"
"twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b)))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
"(λx. twoC(x, 0)) = (λx. (a + (b - a) * x, g2 (a + (b - a) * x)))"
"(λy. twoC(1, y)) = (λx. (b, g2 b + x *⇩R (g1 b - g2 b)))"
"(λx. twoC(x, 1)) = (λx. (a + (b - a) * x, g1 (a + (b - a) * x)))"
"(λy. twoC(0, y)) = (λx. (a, g2 a + x *⇩R (g1 a - g2 a)))"
using assms and typeI_cube_explicit_spec[of"twoC"]
by auto
have bottom_edge_smooth: "(λx. twoC (x, 0)) piecewise_C1_differentiable_on {0..1}"
proof -
have "∀x. (λx. (a + (b - a) * x))-` {x} = {(x - a)/(b -a)}"
using twoCisTypeI(1)
then have finite_vimg: "⋀x. finite({0..1} ∩ (λx. (a + (b - a) * x))-` {x})" by auto
have scale_shif_smth: "(λx. (a + (b - a) * x)) C1_differentiable_on {0..1}" using scale_shift_smooth by auto
then have scale_shif_pw_smth: "(λx. (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}" using C1_differentiable_imp_piecewise by blast
have g2_smooth: "g2 piecewise_C1_differentiable_on (λx. a + (b - a) * x) ` {0..1}" using add_scale_img[OF twoCisTypeI(1)] twoCisTypeI(6) by auto
have "(λx. g2 (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using piecewise_C1_differentiable_compose[OF scale_shif_pw_smth g2_smooth finite_vimg]
then have "(λx::real. (a + (b - a) * x, g2 (a + (b - a) * x))) piecewise_C1_differentiable_on {0..1}"
using all_components_smooth_one_pw_smooth_is_pw_smooth[where f = "(λx::real. (a + (b - a) * x, g2 (a + (b - a) * x)))"]
apply (simp only: real_pair_basis)
by fastforce
then show ?thesis using twoCisTypeI(7) by auto
qed
have top_edge_smooth: "?top_edge piecewise_C1_differentiable_on {0..1}"
proof -
have "∀x. (λx. (a + (b - a) * x))-` {x} = {(x - a)/(b -a)}"
using twoCisTypeI(1)
then have finite_vimg: "⋀x. finite({0..1} ∩ (λx. (a + (b - a) * x))-` {x})" by auto
have scale_shif_smth: "(λx. (a + (b - a) * x)) C1_differentiable_on {0..1}" using scale_shift_smooth by auto
then have scale_shif_pw_smth: "(λx. (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}" using C1_differentiable_imp_piecewise by blast
have g1_smooth: "g1 piecewise_C1_differentiable_on (λx. a + (b - a) * x) ` {0..1}" using add_scale_img[OF twoCisTypeI(1)] twoCisTypeI(5) by auto
have "(λx. g1 (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using piecewise_C1_differentiable_compose[OF scale_shif_pw_smth g1_smooth finite_vimg]
then have "(λx. (a + (b - a) * x, g1 (a + (b - a) * x))) piecewise_C1_differentiable_on {0..1}"
using all_components_smooth_one_pw_smooth_is_pw_smooth[where f = "(λx. (a + (b - a) * x, g1 (a + (b - a) * x)))"]
apply (simp only: real_pair_basis)
by fastforce
then show ?thesis using twoCisTypeI(9) by auto
qed
have right_edge_smooth: "?right_edge piecewise_C1_differentiable_on {0..1}"
proof -
have "(λx. (g2 b + x *⇩R (g1 b - g2 b))) C1_differentiable_on {0..1}"
using scale_shift_smooth C1_differentiable_imp_piecewise by auto
then have "(λx. (g2 b + x *⇩R (g1 b - g2 b))) piecewise_C1_differentiable_on {0..1}"
using C1_differentiable_imp_piecewise by fastforce
then have "(λx. (b, g2 b + x *⇩R (g1 b - g2 b))) piecewise_C1_differentiable_on {0..1}"
using pair_prod_smooth_pw_smooth by auto
then show ?thesis
using twoCisTypeI(8) by auto
qed
have left_edge_smooth: "?left_edge piecewise_C1_differentiable_on {0..1}"
proof -
have "(λx. (g2 a + x *⇩R (g1 a - g2 a))) C1_differentiable_on {0..1}"
using scale_shift_smooth by auto
then have "(λx. (g2 a + x *⇩R (g1 a - g2 a))) piecewise_C1_differentiable_on {0..1}"
using C1_differentiable_imp_piecewise by fastforce
then have "(λx. (a, g2 a + x *⇩R (g1 a - g2 a))) piecewise_C1_differentiable_on {0..1}"
using pair_prod_smooth_pw_smooth by auto
then show ?thesis
using twoCisTypeI(10) by auto
qed
have "γ = ?bottom_edge ∨ γ = ?right_edge ∨ γ = ?top_edge ∨ γ = ?left_edge"
using assms by (auto simp add: boundary_def horizontal_boundary_def vertical_boundary_def)
then show ?thesis
using left_edge_smooth right_edge_smooth top_edge_smooth bottom_edge_smooth by auto
qed

lemma two_chain_integral_eq_integral_divisable:
assumes f_integrable: "∀twoCube ∈ twoChain. F integrable_on cubeImage twoCube" and
gen_division: "gen_division s (cubeImage ` twoChain)" and
valid_two_chain: "valid_two_chain twoChain"
shows "integral s F = two_chain_integral twoChain F"
proof -
show "integral s F = two_chain_integral twoChain F"
have partial_deriv_integrable:
"∀twoCube ∈ twoChain. ((F) has_integral (integral (cubeImage twoCube) (F))) (cubeImage twoCube)"
using f_integrable by auto
then have partial_deriv_integrable:
"⋀twoCubeImg. twoCubeImg ∈ cubeImage ` twoChain ⟹ (F has_integral (integral (twoCubeImg) F)) (twoCubeImg)"
using Henstock_Kurzweil_Integration.integrable_neg by force
have finite_images: "finite (cubeImage ` twoChain)"
using gen_division gen_division_def by auto
have negligible_images: "pairwise (λS S'. negligible (S ∩ S')) (cubeImage ` twoChain)"
using gen_division  by (auto simp add: gen_division_def pairwise_def)
have inj: "inj_on cubeImage twoChain"
using valid_two_chain by (simp add: inj_on_def valid_two_chain_def)
have "integral s F = (∑twoCubeImg∈cubeImage ` twoChain. integral twoCubeImg F)"
using has_integral_Union[OF finite_images partial_deriv_integrable negligible_images] gen_division
also have "… = (∑C∈twoChain. integral (cubeImage C) F)"
using sum.reindex inj by auto
finally show "integral s F = (∑C∈twoChain. integral (cubeImage C) F)" .
qed
qed

definition only_vertical_division where
"only_vertical_division one_chain two_chain ≡
∃𝒱 ℋ. finite ℋ ∧ finite 𝒱 ∧
(∀(k,γ) ∈ 𝒱.
(∃(k',γ') ∈ two_chain_vertical_boundary two_chain.
(∃a ∈ {0..1}. ∃b ∈ {0..1}. a ≤ b ∧ subpath a b γ' = γ))) ∧
(common_sudiv_exists (two_chain_horizontal_boundary two_chain) ℋ
∨ common_reparam_exists ℋ (two_chain_horizontal_boundary two_chain)) ∧
boundary_chain ℋ ∧ one_chain = 𝒱 ∪ ℋ ∧
(∀(k,γ)∈ℋ. valid_path γ)"

abbreviation "valid_typeI_division s twoChain
≡ (∀twoCube ∈ twoChain. typeI_twoCube twoCube) ∧
gen_division s (cubeImage ` twoChain) ∧ valid_two_chain twoChain"

lemma field_cont_on_typeI_region_cont_on_edges:
assumes typeI_twoC: "typeI_twoCube twoC"
and field_cont: "continuous_on (cubeImage twoC) F"
and member_of_boundary: "(k,γ) ∈ boundary twoC"
shows "continuous_on (γ ` {0 .. 1}) F"
proof -
obtain a b g1 g2 where
twoCisTypeI: "a < b"
"(∀x ∈ cbox a b. g2 x ≤ g1 x)"
"cubeImage twoC = {(x,y). x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}"
"twoC = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b)))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
"(λx. twoC(x, 0)) = (λx. (a + (b - a) * x, g2 (a + (b - a) * x)))"
"(λy. twoC(1, y)) = (λx. (b, g2 b + x *⇩R (g1 b - g2 b)))"
"(λx. twoC(x, 1)) = (λx. (a + (b - a) * x, g1 (a + (b - a) * x)))"
"(λy. twoC(0, y)) = (λx. (a, g2 a + x *⇩R (g1 a - g2 a)))"
using typeI_twoC and typeI_cube_explicit_spec[of"twoC"]
by auto
let ?bottom_edge = "(λx. twoC(x, 0))"
let ?right_edge = "(λy. twoC(1, y))"
let ?top_edge = "(λx. twoC(x, 1))"
let ?left_edge = "(λy. twoC(0, y))"
let ?Dg1 =  "{p. ∃x. x ∈ cbox a b ∧ p = (x, g1(x))}"
have line_is_pair_img: "?Dg1 = (λx. (x, g1(x))) ` (cbox a b)"
using image_def by auto
have field_cont_on_top_edge_image: "continuous_on ?Dg1  F"
by (rule continuous_on_subset [OF field_cont]) (auto simp: twoCisTypeI(2) twoCisTypeI(3))
have top_edge_is_compos_of_scal_and_g1:
"(λx. twoC(x, 1)) = (λx. (x, g1(x))) ∘ (λx. a + (b - a) * x)"
using twoCisTypeI  by auto
have Dg1_is_bot_edge_pathimg: "path_image (λx. twoC(x, 1)) = ?Dg1"
using line_is_pair_img and top_edge_is_compos_of_scal_and_g1 image_comp path_image_def add_scale_img and twoCisTypeI(1)
by (metis (no_types, lifting) cbox_interval)
then have cont_on_top: "continuous_on (path_image ?top_edge) F"
using field_cont_on_top_edge_image by auto
let ?Dg2 =  "{p. ∃x. x ∈ cbox a b ∧ p = (x, g2(x))}"
have line_is_pair_img: "?Dg2 = (λx. (x, g2(x))) ` (cbox a b)"
using image_def by auto
have field_cont_on_bot_edge_image: "continuous_on ?Dg2 F"
apply (rule continuous_on_subset [OF field_cont])
using twoCisTypeI(2) twoCisTypeI(3) by auto
have bot_edge_is_compos_of_scal_and_g2: "(λx. twoC(x, 0)) = (λx. (x, g2(x))) ∘ (λx. a + (b - a) * x)"
using twoCisTypeI by auto
have Dg2_is_bot_edge_pathimg:
"path_image (λx. twoC(x, 0)) = ?Dg2"
using line_is_pair_img and bot_edge_is_compos_of_scal_and_g2 image_comp path_image_def add_scale_img and twoCisTypeI(1)
by (metis (no_types, lifting) cbox_interval)
then have cont_on_bot: "continuous_on (path_image ?bottom_edge) F"
using field_cont_on_bot_edge_image by auto
let ?D_left_edge = "{p. ∃y. y ∈ cbox (g2 a) (g1 a) ∧ p = (a, y)}"
have field_cont_on_left_edge_image: "continuous_on ?D_left_edge  F"
apply (rule continuous_on_subset [OF field_cont])
using twoCisTypeI(1) twoCisTypeI(3) by auto
have "g2 a ≤ g1 a" using twoCisTypeI(1) twoCisTypeI(2) by auto
then have "(λx. g2 a + (g1 a - g2 a) * x) ` {(0::real)..1} = {g2 a .. g1 a}"
using add_scale_img'[of "g2 a" "g1 a"] by blast
then have left_eq: "?D_left_edge = ?left_edge ` {0..1}"
unfolding twoCisTypeI(10)
by(auto simp add: subset_iff image_def set_eq_iff Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(7))
then have cont_on_left: "continuous_on (path_image ?left_edge) F"
using field_cont_on_left_edge_image path_image_def
by (metis left_eq field_cont_on_left_edge_image path_image_def)
let ?D_right_edge =  "{p. ∃y. y ∈ cbox (g2 b) (g1 b) ∧ p = (b, y)}"
have field_cont_on_left_edge_image: "continuous_on ?D_right_edge F"
apply (rule continuous_on_subset [OF field_cont])
using twoCisTypeI(1) twoCisTypeI(3) by auto
have "g2 b ≤ g1 b" using twoCisTypeI(1)  twoCisTypeI(2) by auto
then have "(λx. g2 b + (g1 b - g2 b) * x) ` {(0::real)..1} = {g2 b .. g1 b}"
using add_scale_img'[of "g2 b" "g1 b"] by blast
then have right_eq: "?D_right_edge = ?right_edge ` {0..1}"
unfolding twoCisTypeI(8)
by(auto simp add: subset_iff image_def set_eq_iff Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(7))
then have cont_on_right:
"continuous_on (path_image ?right_edge) F"
using field_cont_on_left_edge_image path_image_def
by (metis right_eq field_cont_on_left_edge_image path_image_def)
have all_edge_cases:
"(γ = ?bottom_edge ∨ γ = ?right_edge ∨ γ = ?top_edge ∨ γ = ?left_edge)"
using assms by (auto simp add: boundary_def horizontal_boundary_def vertical_boundary_def)
show ?thesis
using cont_on_top cont_on_bot cont_on_right cont_on_left all_edge_cases
by blast
qed

lemma typeII_cube_explicit_spec:
assumes "typeII_twoCube twoC"
shows "∃a b g1 g2. a < b ∧ (∀x ∈ {a .. b}. g2 x ≤ g1 x) ∧
cubeImage twoC = {(y, x). x ∈ {a..b} ∧ y ∈ {g2 x .. g1 x}}
∧ twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b))
∧ g1 piecewise_C1_differentiable_on {a .. b} ∧ g2 piecewise_C1_differentiable_on {a .. b}
∧ (λx. twoC(0, x)) = (λx. (g2 (a + (b - a) * x), a + (b - a) * x))
∧ (λy. twoC(y, 1)) = (λx. (g2 b + x *⇩R (g1 b - g2 b), b))
∧ (λx. twoC(1, x)) = (λx. (g1 (a + (b - a) * x), a + (b - a) * x))
∧ (λy. twoC(y, 0)) = (λx. (g2 a + x *⇩R (g1 a - g2 a), a))"
proof -
let ?bottom_edge = "(λx. twoC(0, x))"
let ?right_edge = "(λy. twoC(y, 1))"
let ?top_edge = "(λx. twoC(1, x))"
let ?left_edge = "(λy. twoC(y, 0))"
obtain a b g1 g2 where
twoCisTypeII: "a < b"
"(∀x ∈ cbox a b. g2 x ≤ g1 x)"
"cubeImage twoC = {(y, x). x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}"
"twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
using assms and typeII_twoCubeImg[of"twoC"] by auto
have bottom_edge_explicit: "?bottom_edge = (λx. (g2 (a + (b - a) * x), a + (b - a) * x))"
have right_edge_explicit: "?right_edge = (λx. (g2 b + x *⇩R (g1 b - g2 b), b))"
have top_edge_explicit: "?top_edge = (λx. (g1 (a + (b - a) * x), a + (b - a) * x))"
have left_edge_explicit: "?left_edge = (λx. (g2 a + x *⇩R (g1 a - g2 a), a))"
show ?thesis
using bottom_edge_explicit right_edge_explicit top_edge_explicit left_edge_explicit twoCisTypeII
by auto
qed

lemma typeII_twoCube_smooth_edges:
assumes "typeII_twoCube twoC" "(k,γ) ∈ boundary twoC"
shows "γ piecewise_C1_differentiable_on {0..1}"
proof -
let ?bottom_edge = "(λx. twoC(0, x))"
let ?right_edge = "(λy. twoC(y, 1))"
let ?top_edge = "(λx. twoC(1, x))"
let ?left_edge = "(λy. twoC(y, 0))"
obtain a b g1 g2 where
twoCisTypeII: "a < b"
"(∀x ∈ cbox a b. g2 x ≤ g1 x)"
"cubeImage twoC = {(y, x). x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}"
"twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
"(λx. twoC(0, x)) = (λx. (g2 (a + (b - a) * x), a + (b - a) * x))"
"(λy. twoC(y, 1)) = (λx. (g2 b + x *⇩R (g1 b - g2 b), b))"
"(λx. twoC(1, x)) = (λx. (g1 (a + (b - a) * x), a + (b - a) * x))"
"(λy. twoC(y, 0)) = (λx. (g2 a + x *⇩R (g1 a - g2 a), a))"
using assms and typeII_cube_explicit_spec[of"twoC"]
by auto
have bottom_edge_smooth: "?bottom_edge piecewise_C1_differentiable_on {0..1}"
proof -
have "∀x. (λx. (a + (b - a) * x)) -` {x} = {(x - a)/(b -a)}"
using twoCisTypeII(1)  by auto
then have finite_vimg: "⋀x. finite({0..1} ∩ (λx. (a + (b - a) * x))-` {x})" by auto
have scale_shif_pw_smth: "(λx. (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using scale_shift_smooth C1_differentiable_imp_piecewise by blast
have g2_smooth: "g2 piecewise_C1_differentiable_on (λx. a + (b - a) * x) ` {0..1}" using add_scale_img[OF twoCisTypeII(1)] twoCisTypeII(6) by auto
have "(λx. g2 (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using piecewise_C1_differentiable_compose[OF scale_shif_pw_smth g2_smooth finite_vimg]
then have "(λx::real. (g2 (a + (b - a) * x), a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using all_components_smooth_one_pw_smooth_is_pw_smooth[where f = "(λx::real. (g2 (a + (b - a) * x), a + (b - a) * x))"]
then show ?thesis using twoCisTypeII(7) by auto
qed
have top_edge_smooth: "?top_edge piecewise_C1_differentiable_on {0..1}"
proof -
have "∀x. (λx. (a + (b - a) * x))-` {x} = {(x - a)/(b -a)}"
using twoCisTypeII(1) by auto
then have finite_vimg: "⋀x. finite({0..1} ∩ (λx. (a + (b - a) * x))-` {x})" by auto
have scale_shif_pw_smth: "(λx. (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using scale_shift_smooth C1_differentiable_imp_piecewise by blast
have g1_smooth: "g1 piecewise_C1_differentiable_on (λx. a + (b - a) * x) ` {0..1}" using add_scale_img[OF twoCisTypeII(1)] twoCisTypeII(5) by auto
have "(λx. g1 (a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using piecewise_C1_differentiable_compose[OF scale_shif_pw_smth g1_smooth finite_vimg]
then have "(λx::real. (g1 (a + (b - a) * x), a + (b - a) * x)) piecewise_C1_differentiable_on {0..1}"
using all_components_smooth_one_pw_smooth_is_pw_smooth[where f = "(λx::real. (g1 (a + (b - a) * x), a + (b - a) * x))"]
then show ?thesis using twoCisTypeII(9) by auto
qed
have right_edge_smooth: "?right_edge piecewise_C1_differentiable_on {0..1}"
proof -
have "(λx. (g2 b + x *⇩R (g1 b - g2 b))) piecewise_C1_differentiable_on {0..1}"
then have "(λx. (g2 b + x *⇩R (g1 b - g2 b), b)) piecewise_C1_differentiable_on {0..1}"
using all_components_smooth_one_pw_smooth_is_pw_smooth[of "(1,0)" "(λx. (g2 b + x *⇩R (g1 b - g2 b), b))"]
then show ?thesis
using twoCisTypeII(8) by auto
qed
have left_edge_smooth: "?left_edge piecewise_C1_differentiable_on {0..1}"
proof -
have 0: "(λx. (g2 a + x *⇩R (g1 a - g2 a))) C1_differentiable_on {0..1}"
using C1_differentiable_imp_piecewise by fastforce
have "(λx. (g2 a + x *⇩R (g1 a - g2 a), a)) piecewise_C1_differentiable_on {0..1}"
using C1_differentiable_imp_piecewise[OF C1_differentiable_on_pair[OF 0 C1_differentiable_on_const[of "a" "{0..1}"]]]
by force
then show ?thesis
using twoCisTypeII(10) by auto
qed
have "γ = ?bottom_edge ∨ γ = ?right_edge ∨ γ = ?top_edge ∨ γ = ?left_edge"
using assms by (auto simp add: boundary_def horizontal_boundary_def vertical_boundary_def)
then show ?thesis
using left_edge_smooth right_edge_smooth top_edge_smooth bottom_edge_smooth by auto
qed

lemma field_cont_on_typeII_region_cont_on_edges:
assumes typeII_twoC:
"typeII_twoCube twoC" and
field_cont:
"continuous_on (cubeImage twoC) F" and
member_of_boundary:
"(k,γ) ∈ boundary twoC"
shows "continuous_on (γ ` {0 .. 1}) F"
proof -
obtain a b g1 g2 where
twoCisTypeII: "a < b"
"(∀x ∈ cbox a b. g2 x ≤ g1 x)"
"cubeImage twoC = {(y, x). x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}"
"twoC = (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b))"
"g1 piecewise_C1_differentiable_on {a .. b}"
"g2 piecewise_C1_differentiable_on {a .. b}"
"(λx. twoC(0, x)) = (λx. (g2 (a + (b - a) * x), a + (b - a) * x))"
"(λy. twoC(y, 1)) = (λx. (g2 b + x *⇩R (g1 b - g2 b), b))"
"(λx. twoC(1, x)) = (λx. (g1 (a + (b - a) * x), a + (b - a) * x))"
"(λy. twoC(y, 0)) = (λx. (g2 a + x *⇩R (g1 a - g2 a), a))"
using typeII_twoC and typeII_cube_explicit_spec[of"twoC"]
by auto
let ?bottom_edge = "(λx. twoC(0, x))"
let ?right_edge = "(λy. twoC(y, 1))"
let ?top_edge = "(λx. twoC(1, x))"
let ?left_edge = "(λy. twoC(y, 0))"
let ?Dg1 =  "{p. ∃x. x ∈ cbox a b ∧ p = (g1(x), x)}"
have line_is_pair_img: "?Dg1 = (λx. (g1(x), x)) ` (cbox a b)"
using image_def by auto
have field_cont_on_top_edge_image: "continuous_on ?Dg1 F"
by (rule continuous_on_subset [OF field_cont]) (auto simp: twoCisTypeII(2) twoCisTypeII(3))
have top_edge_is_compos_of_scal_and_g1:
"(λx. twoC(1, x)) = (λx. (g1(x), x)) ∘ (λx. a + (b - a) * x)"
using twoCisTypeII by auto
have Dg1_is_bot_edge_pathimg:
"path_image (λx. twoC(1, x)) = ?Dg1"
using line_is_pair_img and top_edge_is_compos_of_scal_and_g1 image_comp path_image_def add_scale_img and twoCisTypeII(1)
by (metis (no_types, lifting) cbox_interval)
then have cont_on_top: "continuous_on (path_image ?top_edge) F"
using field_cont_on_top_edge_image by auto
let ?Dg2 =  "{p. ∃x. x ∈ cbox a b ∧ p = (g2(x), x)}"
have line_is_pair_img: "?Dg2 = (λx. (g2(x), x)) ` (cbox a b)"
using image_def by auto
have field_cont_on_bot_edge_image: "continuous_on ?Dg2 F"
by (rule continuous_on_subset [OF field_cont]) (auto simp add: twoCisTypeII(2) twoCisTypeII(3))
have bot_edge_is_compos_of_scal_and_g2:
"(λx. twoC(0, x)) = (λx. (g2(x), x)) ∘ (λx. a + (b - a) * x)"
using twoCisTypeII by auto
have Dg2_is_bot_edge_pathimg: "path_image (λx. twoC(0, x)) = ?Dg2"
unfolding path_image_def
using line_is_pair_img and bot_edge_is_compos_of_scal_and_g2 image_comp  add_scale_img [OF ‹a < b›]
by (metis (no_types, lifting) box_real(2))
then have cont_on_bot: "continuous_on (path_image ?bottom_edge) F"
using field_cont_on_bot_edge_image
by auto
let ?D_left_edge =  "{p. ∃y. y ∈ cbox (g2 a) (g1 a) ∧ p = (y, a)}"
have field_cont_on_left_edge_image: "continuous_on ?D_left_edge F"
apply (rule continuous_on_subset [OF field_cont])
using twoCisTypeII(1) twoCisTypeII(3) by auto
have "g2 a ≤ g1 a" using twoCisTypeII(1) twoCisTypeII(2) by auto
then have "(λx. g2 a + x * (g1 a - g2 a)) ` {(0::real)..1} = {g2 a .. g1 a}"
with ‹g2 a ≤ g1 a› have left_eq: "?D_left_edge = ?left_edge ` {0..1}"
by (simp only: twoCisTypeII(10)) auto
then have cont_on_left: "continuous_on (path_image ?left_edge) F"
using field_cont_on_left_edge_image path_image_def
by (metis left_eq field_cont_on_left_edge_image path_image_def)
let ?D_right_edge = "{p. ∃y. y ∈ cbox (g2 b) (g1 b) ∧ p = (y, b)}"
have field_cont_on_left_edge_image: "continuous_on ?D_right_edge F"
apply (rule continuous_on_subset [OF field_cont])
using twoCisTypeII(1) twoCisTypeII(3) by auto
have "g2 b ≤ g1 b" using twoCisTypeII(1) twoCisTypeII(2) by auto
then have "(λx. g2 b + x * (g1 b - g2 b)) ` {(0::real)..1} = {g2 b .. g1 b}"
with ‹g2 b ≤ g1 b› have right_eq: "?D_right_edge = ?right_edge ` {0..1}"
by (simp only: twoCisTypeII(8)) auto
then have cont_on_right:
"continuous_on (path_image ?right_edge) F"
using field_cont_on_left_edge_image path_image_def
by (metis right_eq field_cont_on_left_edge_image path_image_def)
have all_edge_cases:
"(γ = ?bottom_edge ∨ γ = ?right_edge ∨ γ = ?top_edge ∨ γ = ?left_edge)"
using assms unfolding boundary_def horizontal_boundary_def vertical_boundary_def by blast
show ?thesis
using cont_on_top cont_on_bot cont_on_right cont_on_left all_edge_cases
by blast
qed

lemma two_cube_boundary_is_boundary: "boundary_chain (boundary C)"
by (auto simp add: boundary_chain_def boundary_def horizontal_boundary_def vertical_boundary_def)

lemma common_boundary_subdiv_exists_refl:
assumes "∀(k,γ)∈boundary twoC. valid_path γ"
shows "common_boundary_sudivision_exists (boundary twoC) (boundary twoC)"
using assms chain_subdiv_chain_refl common_boundary_sudivision_exists_def two_cube_boundary_is_boundary by blast

lemma common_boundary_subdiv_exists_refl':
assumes "∀(k,γ)∈C. valid_path γ"
"boundary_chain (C::(int × (real ⇒ real × real)) set)"
shows "common_boundary_sudivision_exists (C) (C)"
using assms chain_subdiv_chain_refl common_boundary_sudivision_exists_def by blast

lemma gen_common_boundary_subdiv_exists_refl_twochain_boundary:
assumes "∀(k,γ)∈C. valid_path γ"
"boundary_chain (C::(int × (real ⇒ real × real)) set)"
shows "common_sudiv_exists (C) (C)"
using assms chain_subdiv_chain_refl common_boundary_sudivision_exists_def common_subdiv_imp_gen_common_subdiv by blast

lemma two_chain_boundary_is_boundary_chain:
shows "boundary_chain (two_chain_boundary twoChain)"
by (simp add: boundary_chain_def two_chain_boundary_def boundary_def horizontal_boundary_def vertical_boundary_def)

lemma typeI_edges_are_valid_paths:
assumes "typeI_twoCube twoC" "(k,γ) ∈ boundary twoC"
shows "valid_path γ"
using typeI_twoCube_smooth_edges[OF assms] C1_differentiable_imp_piecewise
by (auto simp: valid_path_def)

lemma typeII_edges_are_valid_paths:
assumes "typeII_twoCube twoC" "(k,γ) ∈ boundary twoC"
shows "valid_path γ"
using typeII_twoCube_smooth_edges[OF assms] C1_differentiable_imp_piecewise
by (auto simp: valid_path_def)

lemma finite_two_chain_vertical_boundary:
assumes "finite two_chain"
shows "finite (two_chain_vertical_boundary two_chain)"
using assms  by (simp add: two_chain_vertical_boundary_def vertical_boundary_def)

lemma finite_two_chain_horizontal_boundary:
assumes "finite two_chain"
shows "finite (two_chain_horizontal_boundary two_chain)"
using assms  by (simp add: two_chain_horizontal_boundary_def horizontal_boundary_def)

locale R2 =
fixes i j
assumes i_is_x_axis: "i = (1::real,0::real)" and
j_is_y_axis: "j = (0::real, 1::real)"
begin

lemma analytically_valid_y:
assumes "analytically_valid s F i"
shows "(λx. integral UNIV (λy. (partial_vector_derivative F i) (y, x) * (indicator s (y, x)))) ∈ borel_measurable lborel"
proof -
have "{(1::real, 0::real), (0, 1)} - {(1, 0)} = {(0::real,1::real)}"
by force
with assms show ?thesis
using assms  by(simp add: real_pair_basis analytically_valid_def i_is_x_axis j_is_y_axis)
qed

lemma analytically_valid_x:
assumes "analytically_valid s F j"
shows "(λx. integral UNIV (λy. ((partial_vector_derivative F j) (x, y)) * (indicator s (x, y)))) ∈ borel_measurable lborel"
proof -
have "{(1::real, 0::real), (0, 1)} - {(0, 1)} = {(1::real, 0::real)}"
by force
with assms show ?thesis
by(simp add: real_pair_basis analytically_valid_def i_is_x_axis j_is_y_axis)
qed

lemma Greens_thm_type_I:
fixes F:: "((real*real) ⇒ (real * real))" and
gamma1 gamma2 gamma3 gamma4 :: "(real ⇒ (real * real))" and
a:: "real" and b:: "real" and
g1:: "(real ⇒ real)" and g2:: "(real ⇒ real)"
assumes Dy_def: "Dy_pair = {(x::real,y) . x ∈ cbox a b ∧ y ∈ cbox (g2 x) (g1 x)}" and
gamma1_def: "gamma1 = (λx. (a + (b - a) * x, g2(a + (b - a) * x)))" and
gamma1_smooth: "gamma1 piecewise_C1_differentiable_on {0..1}" and (*TODO: This should be piecewise smooth*)
gamma2_def: "gamma2 = (λx. (b, g2(b) + x  *⇩R (g1(b) - g2(b))))" and
gamma3_def: "gamma3 = (λx. (a + (b - a) * x, g1(a + (b - a) * x)))" and
gamma3_smooth: "gamma3 piecewise_C1_differentiable_on {0..1}" and
gamma4_def: "gamma4 = (λx. (a,  g2(a) + x *⇩R (g1(a) - g2(a))))" and
F_i_analytically_valid: "analytically_valid Dy_pair (λp. F(p) ∙ i) j" and
g2_leq_g1: "∀x ∈ cbox a b. (g2 x) ≤ (g1 x)" and (*This is needed otherwise what would Dy be?*)
a_lt_b: "a < b"
shows "(line_integral F {i} gamma1) +
(line_integral F {i} gamma2) -
(line_integral F {i} gamma3) -
(line_integral F {i} gamma4)
= (integral Dy_pair (λa. - (partial_vector_derivative (λp. F(p) ∙ i) j a)))"
"line_integral_exists F {i} gamma4"
"line_integral_exists F {i} gamma3"
"line_integral_exists F {i} gamma2"
"line_integral_exists F {i} gamma1"
proof -
let ?F_b' = "partial_vector_derivative (λa. (F a) ∙ i)  j"
have F_first_is_continuous: "continuous_on Dy_pair (λa. F(a) ∙ i)"
using F_i_analytically_valid
let ?f = "(λx. if x ∈ (Dy_pair) then (partial_vector_derivative (λa. (F a) ∙ i)  j) x else 0)"
have f_lesbegue_integrable: "integrable lborel ?f"
using F_i_analytically_valid
by (auto simp add: analytically_valid_def indic_ident)
have partially_vec_diff: "∀a ∈ Dy_pair. partially_vector_differentiable (λa. (F a) ∙ i) j a"
using F_i_analytically_valid
by (auto simp add: analytically_valid_def indicator_def)
have x_axis_integral_measurable: "(λx. integral UNIV (λy. ?f(x, y))) ∈ borel_measurable lborel"
proof -
have "(λp. (?F_b' p) * indicator (Dy_pair) p) = (λx. if x ∈ (Dy_pair) then (?F_b') x else 0)"
using indic_ident[of "?F_b'"] by auto
then have "⋀x y. ?F_b' (x,y) * indicator (Dy_pair) (x,y) = (λx. if x ∈ (Dy_pair) then (?F_b') x else 0) (x,y)"
by auto
then show ?thesis
using analytically_valid_x[OF F_i_analytically_valid]