Lean4
/-- The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]` (also called Jacobi identity). -/
theorem leibniz_identity_mlieBracketWithin_apply {U V W : Π (x : M), TangentSpace I x} {s : Set M} {x : M}
(hs : UniqueMDiffOn I s) (h's : x ∈ closure (interior s)) (hx : x ∈ s)
(hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (U x : TangentBundle I M)) s x)
(hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (V x : TangentBundle I M)) s x)
(hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ (W x : TangentBundle I M)) s x) :
mlieBracketWithin I U (mlieBracketWithin I V W s) s x =
mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x :=
by
have A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3 :=
by
simp only [← minSmoothness_add]
exact le_rfl
have s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x :=
inter_mem self_mem_nhdsWithin (nhdsWithin_le_nhds (extChartAt_source_mem_nhds x))
have pre_mem : (extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x :=
by
filter_upwards [s_inter_mem] with y hy
exact
⟨(extChartAt I x).map_source hy.2, by simpa only [mem_preimage, (extChartAt I x).left_inv hy.2] using hy.1⟩
-- write everything as pullbacks of vector fields in `E` (denoted with primes), for which
-- the identity can be checked via direct calculation.
let U' := mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm U (range I)
let V' := mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I)
let W' :=
mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm W
(range I)
-- register basic facts on the pullbacks in the vector space
have J0U :
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun y ↦ (U' y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
contMDiffWithinAt_mpullbackWithin_extChartAt_symm hU hs hx A
have J0V :
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun y ↦ (V' y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx A
have J0W :
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun y ↦ (W' y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
contMDiffWithinAt_mpullbackWithin_extChartAt_symm hW hs hx A
have J1U :
∀ᶠ y in 𝓝[s] x,
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun y ↦ (U' y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x y) :=
eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm hU hs hx A (by simp)
have J1V :
∀ᶠ y in 𝓝[s] x,
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun y ↦ (V' y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x y) :=
eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx A (by simp)
have J1W :
∀ᶠ y in 𝓝[s] x,
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun y ↦ (W' y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x y) :=
eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm hW hs hx A (by simp)
have JU : U =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (extChartAt I x) U' := eventuallyEq_mpullback_mpullbackWithin_extChartAt U
have JV : V =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (extChartAt I x) V' := eventuallyEq_mpullback_mpullbackWithin_extChartAt V
have JW : W =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (extChartAt I x) W' := eventuallyEq_mpullback_mpullbackWithin_extChartAt W
rw [JU.mlieBracketWithin_vectorField_eq_of_mem (JV.mlieBracketWithin_vectorField JW) hx,
(JU.mlieBracketWithin_vectorField JV).mlieBracketWithin_vectorField_eq_of_mem JW hx,
JV.mlieBracketWithin_vectorField_eq_of_mem (JU.mlieBracketWithin_vectorField JW) hx]
/- Rewrite the first term as a pullback-/
have :
∀ᶠ y in 𝓝[s] x,
mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (extChartAt I x) V') (mpullback I 𝓘(𝕜, E) (extChartAt I x) W') s y =
mpullback I 𝓘(𝕜, E) (extChartAt I x)
(mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)) y :=
by
filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem, J1V, J1W,
nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin] with y hy hyV hyW h'y ys
symm
exact
mpullback_mlieBracketWithin (n := minSmoothness 𝕜 2)
(hyV.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness))
(hyW.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness)) hs (contMDiffAt_extChartAt' h'y) ys le_rfl hy
rw [Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem EventuallyEq.rfl this hx, ←
mpullback_mlieBracketWithin (J0U.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness)) _ hs
contMDiffAt_extChartAt hx le_rfl pre_mem];
swap
· apply ContMDiffWithinAt.mdifferentiableWithinAt _ le_rfl
apply J0V.mlieBracketWithin_vectorField J0W (m := 1)
· exact hs.uniqueMDiffOn_target_inter x
· exact ⟨mem_extChartAt_target x, by simp [hx]⟩
· exact le_rfl
have :
∀ᶠ y in 𝓝[s] x,
mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (extChartAt I x) U') (mpullback I 𝓘(𝕜, E) (extChartAt I x) V') s y =
mpullback I 𝓘(𝕜, E) (extChartAt I x)
(mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)) y :=
by
filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem, J1U, J1V,
nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin] with y hy hyU hyV h'y ys
symm
exact
mpullback_mlieBracketWithin (n := minSmoothness 𝕜 2)
(hyU.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness))
(hyV.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness)) hs (contMDiffAt_extChartAt' h'y) ys le_rfl hy
rw [Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem this EventuallyEq.rfl hx, ←
mpullback_mlieBracketWithin _ (J0W.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness)) hs
contMDiffAt_extChartAt hx le_rfl pre_mem];
swap
· apply ContMDiffWithinAt.mdifferentiableWithinAt _ le_rfl
apply J0U.mlieBracketWithin_vectorField J0V (m := 1)
· exact hs.uniqueMDiffOn_target_inter x
· exact ⟨mem_extChartAt_target x, by simp [hx]⟩
· exact le_rfl
have :
∀ᶠ y in 𝓝[s] x,
mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (extChartAt I x) U') (mpullback I 𝓘(𝕜, E) (extChartAt I x) W') s y =
mpullback I 𝓘(𝕜, E) (extChartAt I x)
(mlieBracketWithin 𝓘(𝕜, E) U' W' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)) y :=
by
filter_upwards [eventually_eventually_nhdsWithin.2 pre_mem, J1U, J1W,
nhdsWithin_le_nhds (chart_source_mem_nhds H x), self_mem_nhdsWithin] with y hy hyU hyW h'y ys
symm
exact
mpullback_mlieBracketWithin (n := minSmoothness 𝕜 2)
(hyU.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness))
(hyW.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness)) hs (contMDiffAt_extChartAt' h'y) ys le_rfl hy
rw [Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem EventuallyEq.rfl this hx, ←
mpullback_mlieBracketWithin (J0V.mdifferentiableWithinAt (one_le_two.trans le_minSmoothness)) _ hs
contMDiffAt_extChartAt hx le_rfl pre_mem];
swap
· apply ContMDiffWithinAt.mdifferentiableWithinAt _ le_rfl
apply J0U.mlieBracketWithin_vectorField J0W (m := 1)
· exact hs.uniqueMDiffOn_target_inter x
· exact ⟨mem_extChartAt_target x, by simp [hx]⟩
· exact le_rfl
rw [← mpullback_add_apply, mpullback_apply, mpullback_apply]
congr 1
simp_rw [mlieBracketWithin_eq_lieBracketWithin]
apply leibniz_identity_lieBracketWithin (E := E) le_rfl
· exact hs.uniqueDiffOn_target_inter x
· rw [inter_comm]
exact extChartAt_mem_closure_interior h's (mem_extChartAt_source x)
· exact ⟨mem_extChartAt_target x, by simp [hx]⟩
· exact contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.mp J0U
· exact contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.mp J0V
· exact contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.mp J0W
