Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Let f be a C² embedding of a finite-dimensional manifold M, possibly with boundary or corners, into a finite-dimensional Euclidean space.
Tangent 5 core · 9 supporting The full tangent is the range of the manifold differential of the embedding. ★ chartDifferential_range
Full extrinsic tangent and orthogonal normal spaces
The full tangent is the range of the manifold differential of the embedding. An admissible parametrization is the embedding composed with the inverse of any extended chart in the maximal C² atlas. Derivatives are taken within the extended chart target; this includes boundary points and never substitutes a one-sided tangent cone for the full tangent space.
Federer, Curvature Measures (1959), §§2.8, 4.3–4.6, distinguishes intrinsic tangents from set tangent cones. His normal cone at a boundary is not the orthogonal normal subspace constructed here. Reach results are downstream.
def tangentSpace reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The full extrinsic tangent space is the image of the differential of the embedding.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
x :
M
def
given by
(mfderiv I (modelWithCornersSelf ℝ E) f x).toLinearMap.range
def normalSpace reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The normal space is the orthogonal complement of the full tangent space.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
x :
M
def
given by
(tangentSpace I f x)ᗮ
def chartDifferential reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The chart differential is the derivative within the chart target of its local parametrization.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
φ :
x :
M
def
chartDifferential I f φ x :
F →L[ℝ] E
given by
fderivWithin ℝ (f ∘ (φ.extend I).symm) (φ.extend I).target ((φ.extend I) x)
theorem chartDifferential_range reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
An embedding f satisfying the smooth-embedding condition hf, described by the model with corners I, has the property that the derivative of every admissible chart φ at the point x, under its atlas condition hφ and source condition hx, has range equal to the full extrinsic tangent space.
Formal statement
hypotheses
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
φ :
hφ :
φ ∈ maximalAtlas I 2 M
x :
M
hx :
x ∈ φ.source
conclusion
(chartDifferential I f φ x).toLinearMap.range = tangentSpace I f x
Proof (Lean source)
theorem chartDifferential_range (f : M → E)
(hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f)
(φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M)
(x : M) (hx : x ∈ φ.source) :
(chartDifferential I f φ x).toLinearMap.range = tangentSpace I f x := by
have hd : φ.MDifferentiable I I :=
⟨(contMDiffOn_of_mem_maximalAtlas hφ).mdifferentiableOn (by norm_num),
(contMDiffOn_symm_of_mem_maximalAtlas hφ).mdifferentiableOn (by norm_num)⟩
rw [chartDifferential_eq I f hf φ hφ x hx]
exact LinearMap.range_comp_of_range_eq_top _
(LinearMap.range_eq_top.mpr (hd.symm.mfderiv_surjective (φ.map_source hx)))
def tangentNormalEquiv reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Addition identifies the product of the full tangent and orthogonal normal with the ambient space.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
x :
M
def
given by
(tangentSpace I f x).prodEquivOfIsCompl (normalSpace I f x) (tangent_normal_isCompl I f x)
9 supporting declarations (lemmas, instances)
-
embedding_mfderiv_injectivetheorem — A smooth embedding has an injective manifold differential, including at boundary points.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :MconclusionProof (Lean source)
theorem embedding_mfderiv_injective (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) : Injective (mfderiv I (modelWithCornersSelf ℝ E) f x) := by let h := hf.isImmersion.isImmersionAt x let p : E →L[ℝ] F := (ContinuousLinearMap.fst ℝ F h.complement).comp h.equiv.symm.toContinuousLinearMap let g : E → F := p ∘ (h.codChart.extend (modelWithCornersSelf ℝ E)) have hd : h.domChart.MDifferentiable I I := ⟨(contMDiffOn_of_mem_maximalAtlas h.domChart_mem_maximalAtlas).mdifferentiableOn (by norm_num), (contMDiffOn_symm_of_mem_maximalAtlas h.domChart_mem_maximalAtlas).mdifferentiableOn (by norm_num)⟩ have hg : MDifferentiableAt (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ F) g (f x) := p.hasMFDerivAt.mdifferentiableAt.comp _ ((h.codChart.contMDiffAt_extend h.codChart_mem_maximalAtlas h.mem_codChart_source).mdifferentiableAt (by norm_num)) have heq : g ∘ f =ᶠ[𝓝 x] h.domChart.extend I := by filter_upwards [h.domChart.open_source.mem_nhds h.mem_domChart_source] with y hy have hy' : y ∈ (h.domChart.extend I).source := by simpa using hy have hw := h.writtenInCharts ((h.domChart.extend I).map_source hy') rw [Function.comp_apply, Function.comp_apply, (h.domChart.extend I).left_inv hy'] at hw change p ((h.codChart.extend (modelWithCornersSelf ℝ E)) (f y)) = _ rw [hw] simp [p] have hder : mfderiv I (modelWithCornersSelf ℝ F) (h.domChart.extend I) x = mfderiv I I h.domChart x := by exact (I.hasMFDerivAt.comp x (hd.mdifferentiableAt h.mem_domChart_source).hasMFDerivAt |>.mfderiv).trans (ContinuousLinearMap.id_comp _) have hi : Injective (mfderiv I (modelWithCornersSelf ℝ F) (g ∘ f) x) := by rw [heq.mfderiv_eq, hder] exact hd.mfderiv_injective h.mem_domChart_source rw [mfderiv_comp x hg (hf.contMDiff.mdifferentiable (by norm_num) x)] at hi intro u v huv apply hi change mfderiv (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ F) g (f x) (mfderiv I (modelWithCornersSelf ℝ E) f x u) = _ rw [huv] rfl -
chartDifferential_injectivetheorem — The differential of an admissible chart parametrization is injective on the full model space, including at boundary points.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ :hφ :φ ∈ maximalAtlas I 2 Mx :Mhx :x ∈ φ.sourceconclusionInjective (chartDifferential I f φ x)Proof (Lean source)
theorem chartDifferential_injective (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (x : M) (hx : x ∈ φ.source) : Injective (chartDifferential I f φ x) := by have hd : φ.MDifferentiable I I := ⟨(contMDiffOn_of_mem_maximalAtlas hφ).mdifferentiableOn (by norm_num), (contMDiffOn_symm_of_mem_maximalAtlas hφ).mdifferentiableOn (by norm_num)⟩ rw [chartDifferential_eq I f hf φ hφ x hx] exact (embedding_mfderiv_injective I f hf x).comp (hd.symm.mfderiv_injective (φ.map_source hx)) -
tangentSpace_finranktheorem — The dimension of the full tangent space equals the model dimension.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :MProof (Lean source)
theorem tangentSpace_finrank (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) : finrank ℝ (tangentSpace I f x) = finrank ℝ F := by exact LinearMap.finrank_range_of_inj (f := (mfderiv I (modelWithCornersSelf ℝ E) f x).toLinearMap) (embedding_mfderiv_injective I f hf x) -
tangent_normal_isCompltheorem — Tangent and normal spaces are complementary subspaces of the ambient Euclidean space.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ex :MconclusionIsCompl (tangentSpace I f x) (normalSpace I f x)Proof (Lean source)
theorem tangent_normal_isCompl (f : M → E) (x : M) : IsCompl (tangentSpace I f x) (normalSpace I f x) := (tangentSpace I f x).isCompl_orthogonal -
tangentNormalEquiv_applytheorem — The tangent-normal decomposition equivalence sends a pair to the sum of its ambient vectors.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ex :Mz :tangentSpace I f x × normalSpace I f xconclusiontangentNormalEquiv I f x z = (z.1 : E) + (z.2 : E)Proof (Lean source)
theorem tangentNormalEquiv_apply (f : M → E) (x : M) (z : tangentSpace I f x × normalSpace I f x) : tangentNormalEquiv I f x z = (z.1 : E) + (z.2 : E) := rfl -
tangent_normal_finranktheorem — Tangent and normal dimensions add to the ambient dimension.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ex :Mconclusion= finrank ℝ EProof (Lean source)
theorem tangent_normal_finrank (f : M → E) (x : M) : finrank ℝ (tangentSpace I f x) + finrank ℝ (normalSpace I f x) = finrank ℝ E := (tangentSpace I f x).finrank_add_finrank_orthogonal -
normalSpace_finranktheorem — The normal dimension is the ambient dimension minus the manifold dimension.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :MconclusionProof (Lean source)
theorem normalSpace_finrank (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) : finrank ℝ (normalSpace I f x) = finrank ℝ E - finrank ℝ F := by have h := tangent_normal_finrank I f x rw [tangentSpace_finrank I f hf x] at h omega -
continuous_tangentProjectiontheorem — The ambient orthogonal projection onto the full tangent varies continuously with the base point.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fconclusionContinuous (fun x => (tangentSpace I f x).starProjection)Proof (Lean source)
theorem continuous_tangentProjection (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) : Continuous (fun x => (tangentSpace I f x).starProjection) := by classical rw [continuous_iff_continuousAt] intro x let φ := chartAt H x have hφ : φ ∈ maximalAtlas I 2 M := IsManifold.chart_mem_maximalAtlas x have hx : x ∈ φ.source := mem_chart_source H x let A : F →L[ℝ] E := mfderiv I (modelWithCornersSelf ℝ E) f x -- Use the fixed tangent fiber as an inner-product domain without changing the norm on F. let V := A.range let e : F ≃L[ℝ] V := (LinearEquiv.ofInjective A.toLinearMap (embedding_mfderiv_injective I f hf x)).toContinuousLinearEquiv let D : M → V →L[ℝ] E := fun y => (chartDifferential I f φ y).comp e.symm.toContinuousLinearMap have hd : φ.MDifferentiable I I := ⟨(contMDiffOn_of_mem_maximalAtlas hφ).mdifferentiableOn (by norm_num), (contMDiffOn_symm_of_mem_maximalAtlas hφ).mdifferentiableOn (by norm_num)⟩ have hinj : ∀ y ∈ φ.source, Injective (D y) := by intro y hy dsimp only [D] rw [chartDifferential_eq I f hf φ hφ y hy] exact (embedding_mfderiv_injective I f hf y).comp ((hd.symm.mfderiv_injective (φ.map_source hy)).comp e.symm.injective) have hu : UniqueDiffOn ℝ (φ.extend I).target := by rw [φ.extend_target] exact I.uniqueDiffOn_preimage φ.open_target have hp : ContDiffOn ℝ 2 (f ∘ (φ.extend I).symm) (φ.extend I).target := by apply ContMDiffOn.contDiffOn rw [φ.extend_target'] exact hf.contMDiff.comp_contMDiffOn (contMDiffOn_extend_symm hφ) have hc : ContinuousOn (fun y => chartDifferential I f φ y) φ.source := (hp.continuousOn_fderivWithin hu (by norm_num)).comp (φ.contMDiffOn_extend hφ).continuousOn (fun y hy => (φ.extend I).map_source (by simpa using hy)) have hD : ContinuousAt D x := by exact ((hc.clm_comp (show ContinuousOn (fun _ : M => e.symm.toContinuousLinearMap) φ.source from continuousOn_const)) x hx).continuousAt (φ.open_source.mem_nhds hx) have ha : ContinuousAt (fun y => adjoint (D y)) x := ContinuousLinearMap.adjoint.continuous.continuousAt.comp hD have hg := ha.clm_comp hD have hi : ContinuousAt (fun y => ((adjoint (D y)).comp (D y)).inverse) x := ((gram_isInvertible (D x) (hinj x hx)).contDiffAt_map_inverse (n := 0)).continuousAt.comp (f := fun y => (adjoint (D y)).comp (D y)) hg apply (hD.clm_comp (hi.clm_comp ha)).congr_of_eventuallyEq filter_upwards [φ.open_source.mem_nhds hx] with y hy have hr : (D y).range = tangentSpace I f y := by change ((chartDifferential I f φ y).comp e.symm.toContinuousLinearMap).range = _ rw [ContinuousLinearMap.toLinearMap_comp] exact (LinearMap.range_comp_of_range_eq_top (chartDifferential I f φ y).toLinearMap (LinearMap.range_eq_top.mpr e.symm.surjective)).trans (chartDifferential_range I f hf φ hφ y hy) rw [← hr, starProjection_range_eq (D y) (hinj y hy)] -
continuous_normalProjectiontheorem — The ambient orthogonal projection onto the normal varies continuously with the base point.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fconclusionProof (Lean source)
theorem continuous_normalProjection (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) : Continuous (fun x => (normalSpace I f x).starProjection) := by simp_rw [normalSpace, Submodule.starProjection_orthogonal] convert ((continuous_const (y := id ℝ E)).sub (continuous_tangentProjection I f hf)) using 1 rfl
NormalBundle 11 core · 22 supporting This module supplies closed normal disk bundles, normal coordinates, and ambient Euclidean volume measures on varying finite-dimensional normal fibers. ★ lintegral_normalDiskReferenceMeasure
Normal disk bundles and fiber volume
This module supplies closed normal disk bundles, normal coordinates, and ambient Euclidean volume measures on varying finite-dimensional normal fibers. Continuous projection families yield measurable finite kernels and iterated integration formulas; the embedded-manifold interface specializes these results to C² Euclidean embeddings, including boundary and zero-codimension cases.
def normalDiskSet reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The closed unit normal disk bundle of a family of subspaces over a base consists of the pairs of a base point and an ambient vector orthogonal to the subspace at that point with norm at most one.
abbrev NormalDiskBundle reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The closed unit normal disk bundle of a family of subspaces over a base, as a space: the pairs of a base point and an ambient vector that is orthogonal to the subspace at that point and has norm at most one, with the topology inherited from base times ambient space.
Definition (Lean source)
def normalCoordinate reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Normal coordinates add a scaled fiber vector to the embedded base point.
Definition (Lean source)
parameters
def
normalCoordinate T f a z :
E
given by
f z.val.1 + a • z.val.2
def fiberVolume reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Fiber volume is intrinsic Euclidean volume pushed forward by inclusion into the ambient space.
def fiberDiskVolume reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The fiber disk volume restricts intrinsic fiber volume to the ambient closed unit ball.
Definition (Lean source)
def fiberVolumeKernel reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The varying Euclidean fiber volumes form a measurable kernel into the ambient space.
Definition (Lean source)
parameters
E :
Type u_1
X :
Type u_2
P :
X → Submodule ℝ E
hP :
Continuous (fun x => (P x).starProjection)
def
given by
⟨fun x => fiberVolume (P x), measurable_fiberVolume P hP⟩
def fiberDiskVolumeKernel reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The varying unit fiber disks form a measurable kernel into the ambient space.
Definition (Lean source)
parameters
E :
Type u_1
X :
Type u_2
P :
X → Submodule ℝ E
hP :
Continuous (fun x => (P x).starProjection)
def
given by
⟨fun x => fiberDiskVolume (P x), measurable_fiberDiskVolume P hP⟩
def normalFiberVolumeKernel reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Intrinsic Euclidean volumes of all normal fibers form a measurable kernel.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
def
given by
def normalDiskVolumeKernel reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Euclidean volumes on the closed unit normal fibers form a measurable finite kernel.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
def
given by
def normalDiskReferenceMeasure reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The tube reference measure is the base measure combined with Euclidean unit normal disk volumes.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
μ :
Measure M
def
given by
μ ⊗ₘ normalDiskVolumeKernel I f hf
theorem lintegral_normalDiskReferenceMeasure reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
A model with corners I, a smooth Euclidean embedding f with certificate hf, an s-finite base measure μ, and a nonnegative measurable integrand g with measurability certificate hg give integration against the normal-disk reference measure equal to iterated integration over the base and its normal fibers.
Formal statement
hypotheses
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
g :
M × E → ℝ≥0∞
hg :
conclusion
∫⁻ z, g z ∂normalDiskReferenceMeasure I f hf μ
= ∫⁻ x, ∫⁻ u, g (x, u) ∂fiberDiskVolume (normalSpace I f x) ∂μ
Proof (Lean source)
theorem lintegral_normalDiskReferenceMeasure (f : M → E)
(hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (μ : Measure M) [SFinite μ]
(g : M × E → ℝ≥0∞) (hg : Measurable g) :
∫⁻ z, g z ∂normalDiskReferenceMeasure I f hf μ =
∫⁻ x, ∫⁻ u, g (x, u) ∂fiberDiskVolume (normalSpace I f x) ∂μ :=
lintegral_fiberDiskVolume_compProd _ _ μ g hg
22 supporting declarations (lemmas, instances)
-
finrank_eq_of_projection_closetheorem — Orthogonal projections less than one apart in operator norm have subspaces of equal dimension.hypothesesProof (Lean source)
theorem finrank_eq_of_projection_close (P Q : Submodule ℝ E) (h : ‖P.starProjection - Q.starProjection‖ < 1) : finrank ℝ P = finrank ℝ Q := by apply Nat.le_antisymm · exact LinearMap.finrank_le_finrank_of_injective (projection_restriction_injective P Q h) · exact LinearMap.finrank_le_finrank_of_injective (projection_restriction_injective Q P (by simpa [norm_sub_rev] using h)) -
exists_local_isometricFrametheorem — A continuous projection family admits a local continuous isometric frame onto each fiber.hypothesesE :sharedType u_1X :sharedType u_2P :X → Submodule ℝ EhP :Continuous (fun x => (P x).starProjection)x :Xconclusionconclusion 1∃ e : X → ((P x) →L[ℝ] E),ContinuousOn e Uy ∈ U :Isometry (e y)(e y).toLinearMap.range = P yProof (Lean source)
theorem exists_local_isometricFrame (P : X → Submodule ℝ E) (hP : Continuous (fun x => (P x).starProjection)) (x : X) : ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∃ e : X → ((P x) →L[ℝ] E), ContinuousOn e U ∧ ∀ y ∈ U, Isometry (e y) ∧ (e y).toLinearMap.range = P y := by classical let U : Set X := {y | ‖(P x).starProjection - (P y).starProjection‖ < 1} have hU : IsOpen U := isOpen_lt (continuous_const.sub hP).norm continuous_const have hx : x ∈ U := by simp [U] let b := stdOrthonormalBasis ℝ (P x) let f : X → Fin (finrank ℝ (P x)) → E := fun y i => (P y).starProjection (b i : E) have hf : ∀ i, ContinuousOn (fun y => f y i) U := fun i => (hP.clm_apply continuous_const).continuousOn have hi : ∀ y ∈ U, LinearIndependent ℝ (f y) := by intro y hy let L := (P y).orthogonalProjectionOnto.comp (P x).subtypeL have hL := projection_restriction_injective (P x) (P y) hy have hli := b.toBasis.linearIndependent.map' L.toLinearMap (LinearMap.ker_eq_bot.mpr hL) exact hli.map' (P y).subtype (LinearMap.ker_eq_bot.mpr (Submodule.injective_subtype _)) let g := fun y => InnerProductSpace.gramSchmidtNormed ℝ (f y) let e : X → ((P x) →L[ℝ] E) := fun y => (b.toBasis.constr ℝ (g y)).toContinuousLinearMap refine ⟨U, hU, hx, e, ?_, ?_⟩ · apply continuousOn_clm_apply.mpr intro v change ContinuousOn (fun y => b.toBasis.constr ℝ (g y) v) U simp_rw [Module.Basis.constr_apply_fintype] apply continuousOn_finsetSum intro i _ exact continuousOn_const.smul (continuousOn_gramSchmidtNormed f hf hi i) · intro y hy have ho := InnerProductSpace.gramSchmidtNormed_orthonormal (hi y hy) have heiso : Isometry (e y) := by have horth : Orthonormal ℝ ((b.toBasis.constr ℝ (g y)) ∘ b.toBasis) := by simpa only [Function.comp_def, Module.Basis.constr_basis] using ho exact ((b.toBasis.constr ℝ (g y)).isometryOfOrthonormal b.orthonormal horth).isometry refine ⟨heiso, ?_⟩ have hspan : (e y).toLinearMap.range = span ℝ (range (f y)) := by change (b.toBasis.constr ℝ (g y)).range = _ rw [Module.Basis.constr_range, InnerProductSpace.span_gramSchmidtNormed_range, InnerProductSpace.span_gramSchmidt] apply Submodule.eq_of_le_of_finrank_eq · rw [hspan] apply Submodule.span_le.mpr rintro _ ⟨i, rfl⟩ exact (P y).starProjection_apply_mem _ · rw [LinearMap.finrank_range_of_inj heiso.injective] exact finrank_eq_of_projection_close (P x) (P y) hy -
isClosed_normalDiskSettheorem — A continuous tangent projection makes the unit normal disk bundle closed in base times ambient space.hypothesesX :sharedType u_1E :sharedType u_2T :X → Submodule ℝ EhT :Continuous (fun x => (T x).starProjection)conclusionProof (Lean source)
theorem isClosed_normalDiskSet (T : X → Submodule ℝ E) (hT : Continuous (fun x => (T x).starProjection)) : IsClosed (normalDiskSet T) := by have hp : Continuous (fun z : X × E => (T z.1).starProjection z.2) := (hT.comp continuous_fst).clm_apply continuous_snd have hn : Continuous (fun z : X × E => ‖z.2‖) := continuous_snd.norm convert (isClosed_eq hp (continuous_const (y := (0 : E)))).inter (isClosed_le hn (continuous_const (y := (1 : ℝ)))) using 1 ext z simp only [normalDiskSet, Set.mem_ofPred_eq, Set.mem_inter_iff, Submodule.starProjection_apply_eq_zero_iff] -
continuous_normalCoordinatetheorem — The normal-coordinate map is continuous for every real scaling parameter.hypothesesconclusionContinuous (normalCoordinate T f a)Proof (Lean source)
@[fun_prop] theorem continuous_normalCoordinate (T : X → Submodule ℝ E) (f : X → E) (hf : Continuous f) (a : ℝ) : Continuous (normalCoordinate T f a) := by exact (hf.comp (continuous_fst.comp continuous_subtype_val)).add ((continuous_snd.comp continuous_subtype_val).const_smul a) -
measurableSet_normalDiskSettheorem — The unit normal disk bundle is a Borel subset of base times ambient space.hypothesesX :sharedType u_1E :sharedType u_2T :X → Submodule ℝ EhT :Continuous (fun x => (T x).starProjection)conclusionProof (Lean source)
theorem measurableSet_normalDiskSet (T : X → Submodule ℝ E) (hT : Continuous (fun x => (T x).starProjection)) : MeasurableSet (normalDiskSet T) := (isClosed_normalDiskSet T hT).measurableSet -
measurable_normalCoordinatetheorem — Continuous normal coordinates are Borel measurable on the normal disk bundle.hypothesesconclusionMeasurable (normalCoordinate T f a)Proof (Lean source)
@[fun_prop] theorem measurable_normalCoordinate (T : X → Submodule ℝ E) (f : X → E) (hf : Continuous f) (a : ℝ) : Measurable (normalCoordinate T f a) := (continuous_normalCoordinate T f hf a).measurable -
plane_volume_eq_hausdorfftheorem — Intrinsic Euclidean volume on a plane is its normalized Hausdorff measure of the plane dimension.hypothesesE :sharedType u_1K :Submodule ℝ EProof (Lean source)
theorem plane_volume_eq_hausdorff (K : Submodule ℝ E) : (volume : Measure K) = Measure.euclideanHausdorffMeasure (finrank ℝ K) := InnerProductSpace.euclideanHausdorffMeasure_eq_volume.symm -
fiberVolume_eq_hausdorfftheorem — The ambient fiber volume is normalized Hausdorff measure restricted to the isometric plane.Proof (Lean source)
theorem fiberVolume_eq_hausdorff (K : Submodule ℝ E) : fiberVolume K = (Measure.euclideanHausdorffMeasure (finrank ℝ K) : Measure E).restrict K := by unfold fiberVolume rw [plane_volume_eq_hausdorff] have h : Isometry (fun v : K => (v : E)) := fun _ _ => rfl simpa using h.map_euclideanHausdorffMeasure (d := finrank ℝ K) -
fiberVolume_bottheorem — Zero-dimensional normal volume is the unit point mass at the zero vector.Proof (Lean source)
theorem fiberVolume_bot : fiberVolume (⊥ : Submodule ℝ E) = Measure.dirac 0 := by rw [fiberVolume_eq_hausdorff] simp only [finrank_bot, Measure.euclideanHausdorffMeasure_zero, Submodule.bot_coe, Measure.restrict_singleton, Measure.hausdorffMeasure_zero_singleton, one_smul] -
fiberDiskVolume_finitetheorem — Every closed unit fiber disk has finite Euclidean volume, including the zero-dimensional disk.Proof (Lean source)
theorem fiberDiskVolume_finite (K : Submodule ℝ E) : fiberDiskVolume K univ < ⊤ := by unfold fiberDiskVolume fiberVolume rw [Measure.restrict_apply_univ, Measure.map_apply continuous_subtype_val.measurable measurableSet_closedBall] have hpre : (fun v : K => (v : E)) ⁻¹' closedBall 0 1 = closedBall (0 : K) 1 := by ext v simp [Metric.mem_closedBall, dist_zero_right] rw [hpre] exact (isCompact_closedBall (0 : K) 1).measure_lt_top -
fiberDiskVolume_ae_memtheorem — Fiber disk volume is supported on vectors in the fiber with norm at most one.hypothesesE :sharedType u_1K :Submodule ℝ Econclusion∀ᵐ u ∂fiberDiskVolume K, u ∈ K ∧ ‖u‖ ≤ 1Proof (Lean source)
theorem fiberDiskVolume_ae_mem (K : Submodule ℝ E) : ∀ᵐ u ∂fiberDiskVolume K, u ∈ K ∧ ‖u‖ ≤ 1 := by have hK : ∀ᵐ u ∂fiberVolume K, u ∈ K := by rw [fiberVolume_eq_hausdorff] exact ae_restrict_mem K.closed_of_finiteDimensional.measurableSet filter_upwards [ae_restrict_of_ae hK, ae_restrict_mem (μ := fiberVolume K) measurableSet_closedBall] with u hu hball exact ⟨hu, by simpa [Metric.mem_closedBall, dist_zero_right] using hball⟩ -
fiberDiskVolume_uniform_boundtheorem — The volumes of unit disks in all subspaces have one finite ambient-dimension bound.hypothesesE :sharedType u_1Proof (Lean source)
theorem fiberDiskVolume_uniform_bound : ∃ C : ℝ≥0∞, C < ⊤ ∧ ∀ K : Submodule ℝ E, fiberDiskVolume K univ ≤ C := by classical let V : ℕ → ℝ≥0∞ := fun d => volume (closedBall (0 : EuclideanSpace ℝ (Fin d)) 1) have hV (d : ℕ) : V d < ⊤ := (isCompact_closedBall (0 : EuclideanSpace ℝ (Fin d)) 1).measure_lt_top have hmass (K : Submodule ℝ E) : fiberDiskVolume K univ = V (finrank ℝ K) := by unfold fiberDiskVolume fiberVolume rw [Measure.restrict_apply_univ, Measure.map_apply continuous_subtype_val.measurable measurableSet_closedBall] have hpre : (fun v : K => (v : E)) ⁻¹' closedBall 0 1 = closedBall (0 : K) 1 := by ext v simp [Metric.mem_closedBall, dist_zero_right] rw [hpre, ← (stdOrthonormalBasis ℝ K).measurePreserving_repr_symm.measure_preimage measurableSet_closedBall.nullMeasurableSet] simp only [LinearIsometryEquiv.preimage_closedBall, LinearIsometryEquiv.symm_symm, map_zero] rfl refine ⟨∑ d : Fin (finrank ℝ E + 1), V d, ?_, ?_⟩ · exact ENNReal.sum_lt_top.mpr fun d _ => hV d · intro K rw [hmass K] let d : Fin (finrank ℝ E + 1) := ⟨Module.finrank ℝ K, Nat.lt_succ_of_le K.finrank_le⟩ change V (d : ℕ) ≤ ∑ i : Fin (finrank ℝ E + 1), V (i : ℕ) exact Finset.single_le_sum (s := univ) (a := d) (f := fun i : Fin (finrank ℝ E + 1) => V (i : ℕ)) (fun _ _ => zero_le) (Finset.mem_univ d) -
measurable_fiberVolumetheorem — Continuous orthogonal projections give a measurable family of intrinsic ambient fiber volumes.hypothesesE :sharedType u_1X :sharedType u_2P :X → Submodule ℝ EhP :Continuous (fun x => (P x).starProjection)conclusionMeasurable (fun x => fiberVolume (P x))Proof (Lean source)
@[fun_prop] theorem measurable_fiberVolume (P : X → Submodule ℝ E) (hP : Continuous (fun x => (P x).starProjection)) : Measurable (fun x => fiberVolume (P x)) := by classical -- Work on the second-countable image of the projection operator, rather than X. let S : Set (E →L[ℝ] E) := range (fun K : Submodule ℝ E => K.starProjection) let : MeasurableSpace (E →L[ℝ] E) := borel (E →L[ℝ] E) have : BorelSpace (E →L[ℝ] E) := ⟨rfl⟩ let Q : S → Submodule ℝ E := fun y => y.property.choose have hQ (y : S) : (Q y).starProjection = y.val := y.property.choose_spec have hQc : Continuous (fun y => (Q y).starProjection) := by simpa only [hQ] using (continuous_subtype_val : Continuous (fun y : S => y.val)) have hlocal (x : S) : ∃ U : Set S, IsOpen U ∧ x ∈ U ∧ Measurable (fun y : U => fiberVolume (Q y)) := by obtain ⟨U, hU, hx, e, he, heiso⟩ := exists_local_isometricFrame Q hQc x refine ⟨U, hU, hx, ?_⟩ have hmap (y : U) : Measure.map (e y) volume = fiberVolume (Q y) := by obtain ⟨hi, hr⟩ := heiso y y.property have hd : finrank ℝ (Q x) = finrank ℝ (Q y) := by rw [← hr, LinearMap.finrank_range_of_inj hi.injective] rw [plane_volume_eq_hausdorff, hi.map_euclideanHausdorffMeasure, fiberVolume_eq_hausdorff, hd] congr 1 exact congrArg (fun K : Submodule ℝ E => (K : Set E)) hr have hj : Measurable (fun z : U × Q x => e z.1 z.2) := ((he.domRestrict.comp continuous_fst).clm_apply continuous_snd).measurable apply Measure.measurable_of_measurable_coe intro A hA have hm := measurable_measure_prodMk_left (ν := (volume : Measure (Q x))) (hA.preimage hj) have hemeas (y : U) : Measurable (e y) := (e y).continuous.measurable simpa only [← hmap, Measure.map_apply (hemeas _) hA, Set.preimage_preimage, Function.comp_def] using hm choose U hU hx hmeas using hlocal obtain ⟨t, ht, hcover⟩ := countable_cover_nhds (fun x => (hU x).mem_nhds (hx x)) have hmeasQ : Measurable (fun y => fiberVolume (Q y)) := by intro A hA have hpre : (fun y => fiberVolume (Q y)) ⁻¹' A = ⋃ x ∈ t, ((↑) : U x → S) '' ((fun y : U x => fiberVolume (Q y)) ⁻¹' A) := by ext y constructor · intro hy have hycover : y ∈ ⋃ x ∈ t, U x := by rw [hcover]; trivial obtain ⟨x, hxt, hyU⟩ := Set.mem_iUnion₂.mp hycover exact Set.mem_iUnion₂.mpr ⟨x, hxt, ⟨⟨y, hyU⟩, hy, rfl⟩⟩ · intro hy obtain ⟨x, _, z, hz, rfl⟩ := Set.mem_iUnion₂.mp hy exact hz rw [hpre] exact MeasurableSet.biUnion ht (fun x _ => (hU x).measurableSet.subtype_image (hmeas x hA)) let f : X → S := fun x => ⟨(P x).starProjection, ⟨P x, rfl⟩⟩ have hf : Measurable f := hP.measurable.subtype_mk have hQP (x : X) : Q (f x) = P x := by have hh : (Q (f x)).starProjection = (P x).starProjection := hQ (f x) have hr := congrArg (fun L : E →L[ℝ] E => L.toLinearMap.range) hh simpa only [Submodule.range_starProjection] using hr simpa only [Function.comp_def, hQP] using hmeasQ.comp hf -
measurable_fiberDiskVolumetheorem — Continuous orthogonal projections give a measurable family of closed unit fiber disk volumes.hypothesesE :sharedType u_1X :sharedType u_2P :X → Submodule ℝ EhP :Continuous (fun x => (P x).starProjection)conclusionMeasurable (fun x => fiberDiskVolume (P x))Proof (Lean source)
@[fun_prop] theorem measurable_fiberDiskVolume (P : X → Submodule ℝ E) (hP : Continuous (fun x => (P x).starProjection)) : Measurable (fun x => fiberDiskVolume (P x)) := by apply Measure.measurable_of_measurable_coe intro A hA simpa only [fiberDiskVolume, Measure.restrict_apply hA, Function.comp_def] using (Measure.measurable_coe (hA.inter measurableSet_closedBall)).comp (measurable_fiberVolume P hP) -
fiberDiskVolumeKernel_isFiniteinstance — The disk-volume kernel is uniformly finite and hence supports kernel Fubini integration.parametersE :sharedType u_1X :sharedType u_2P :X → Submodule ℝ EhP :Continuous (fun x => (P x).starProjection)instancegiven byby obtain ⟨C, hC, hbound⟩ := fiberDiskVolume_uniform_bound (E := E) exact ⟨⟨C, hC, fun x=> hbound (P x)⟩⟩ -
measurable_lintegral_fiberDiskVolumetheorem — Integrating a nonnegative jointly measurable function over varying fiber disks gives a measurable base function.hypothesesE :sharedType u_1X :sharedType u_2P :X → Submodule ℝ EhP :Continuous (fun x => (P x).starProjection)g :X × E → ℝ≥0∞hg :conclusionMeasurable (fun x => ∫⁻ u, g (x, u) ∂fiberDiskVolume (P x))Proof (Lean source)
theorem measurable_lintegral_fiberDiskVolume (P : X → Submodule ℝ E) (hP : Continuous (fun x => (P x).starProjection)) (g : X × E → ℝ≥0∞) (hg : Measurable g) : Measurable (fun x => ∫⁻ u, g (x, u) ∂fiberDiskVolume (P x)) := by exact hg.lintegral_kernel_prod_right' (κ := fiberDiskVolumeKernel P hP) -
lintegral_fiberDiskVolume_compProdtheorem — Integration over the base-disk measure equals iterated integration over base and normal fibers.hypothesesE :sharedType u_1X :sharedType u_2P :X → Submodule ℝ EhP :Continuous (fun x => (P x).starProjection)g :X × E → ℝ≥0∞hg :conclusion∫⁻ z, g z ∂(μ ⊗ₘ fiberDiskVolumeKernel P hP)= ∫⁻ x, ∫⁻ u, g (x, u) ∂fiberDiskVolume (P x) ∂μProof (Lean source)
theorem lintegral_fiberDiskVolume_compProd (P : X → Submodule ℝ E) (hP : Continuous (fun x => (P x).starProjection)) (μ : Measure X) [SFinite μ] (g : X × E → ℝ≥0∞) (hg : Measurable g) : ∫⁻ z, g z ∂(μ ⊗ₘ fiberDiskVolumeKernel P hP) = ∫⁻ x, ∫⁻ u, g (x, u) ∂fiberDiskVolume (P x) ∂μ := by exact Measure.lintegral_compProd hg -
embedding_normalDiskSet_isClosedtheorem — The normal disk bundle of a C² embedding is closed relative to manifold times ambient space.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fconclusionIsClosed (normalDiskSet (tangentSpace I f))Proof (Lean source)
theorem embedding_normalDiskSet_isClosed (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) : IsClosed (normalDiskSet (tangentSpace I f)) := isClosed_normalDiskSet _ (continuous_tangentProjection I f hf) -
embedding_normalDiskSet_measurabletheorem — The embedded normal disk bundle is a Borel subset of manifold times ambient space.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fconclusionMeasurableSet (normalDiskSet (tangentSpace I f))Proof (Lean source)
theorem embedding_normalDiskSet_measurable (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) : MeasurableSet (normalDiskSet (tangentSpace I f)) := (embedding_normalDiskSet_isClosed I f hf).measurableSet -
embedding_normalCoordinate_continuoustheorem — Normal coordinates of a C² embedding are continuous on its unit normal disk bundle.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fa :ℝconclusionContinuous (normalCoordinate (tangentSpace I f) f a)Proof (Lean source)
theorem embedding_normalCoordinate_continuous (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (a : ℝ) : Continuous (normalCoordinate (tangentSpace I f) f a) := continuous_normalCoordinate _ f hf.contMDiff.continuous a -
embedding_normalCoordinate_measurabletheorem — Normal coordinates of a C² embedding are Borel measurable on its unit normal disk bundle.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fa :ℝconclusionMeasurable (normalCoordinate (tangentSpace I f) f a)Proof (Lean source)
theorem embedding_normalCoordinate_measurable (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (a : ℝ) : Measurable (normalCoordinate (tangentSpace I f) f a) := (embedding_normalCoordinate_continuous I f hf a).measurable -
normalDiskVolumeKernel_isFiniteinstance — The normal disk kernel is uniformly finite over the embedded manifold.parametersF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 finstancegiven by
ShapeOperator 9 core · 18 supporting This module develops the normal-valued second fundamental form of a finite-dimensional Euclidean C² embedded manifold, including model-with-corners boundary points. ★ secondFundamentalForm_chart
Second fundamental forms and shape operators
This module develops the normal-valued second fundamental form of a finite-dimensional Euclidean C² embedded manifold, including model-with-corners boundary points. It also provides the algebraic shape operator and its determinant interface. All constructions are chart independent.
def scalarSecondForm reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
Pairing a normal-valued bilinear form with a normal vector gives a scalar bilinear form.
Definition (Lean source)
parameters
T :
Type u_1
N :
Type u_2
B :
T →L[ℝ] T →L[ℝ] N
u :
N
def
scalarSecondForm B u :
T →L[ℝ] T →L[ℝ] ℝ
given by
((innerSL ℝ u).postcomp T).comp B
def shapeOperator reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The shape operator of a normal-valued bilinear form B in a normal direction u is the linear map S on the tangent space with ⟨S v, w⟩ = ⟨u, B(v, w)⟩ for all tangent vectors v and w, that is, the Riesz representative of the scalar second form in its second argument.
Definition (Lean source)
parameters
T :
Type u_1
N :
Type u_2
B :
T →L[ℝ] T →L[ℝ] N
u :
N
def
shapeOperator B u :
T →L[ℝ] T
given by
InnerProductSpace.continuousLinearMapOfBilin (scalarSecondForm B u)
def tubeDeterminant reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The signed normal tube factor is the intrinsic determinant of identity minus the scaled shape operator.
Definition (Lean source)
parameters
T :
Type u_1
N :
Type u_2
B :
T →L[ℝ] T →L[ℝ] N
a :
ℝ
u :
N
def
tubeDeterminant B a u :
ℝ
given by
def chartHessian reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The local parametrization Hessian is its iterated derivative within the extended chart target.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
φ :
x :
M
def
chartHessian I f φ x :
F →L[ℝ] F →L[ℝ] E
given by
fderivWithin ℝ (fun y => fderivWithin ℝ (f ∘ (φ.extend I).symm) (φ.extend I).target y) (φ.extend I).target ((φ.extend I) x)
def chartTangentVector reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
A chart model vector maps to a vector of the full extrinsic tangent space.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
φ :
hφ :
φ ∈ maximalAtlas I 2 M
x :
M
hx :
x ∈ φ.source
v :
F
def
chartTangentVector I f hf φ hφ x hx v :
tangentSpace I f x
given by
⟨chartDifferential I f φ x v, by rw [← chartDifferential_range I f hf φ hφ x hx] exact ⟨v, rfl⟩⟩
def chartTangentEquiv reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
An admissible parametrization differential continuously identifies the full model space with the full extrinsic tangent space.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
φ :
hφ :
φ ∈ maximalAtlas I 2 M
x :
M
hx :
x ∈ φ.source
def
chartTangentEquiv I f hf φ hφ x hx :
F ≃L[ℝ] tangentSpace I f x
given by
by let L : F →ₗ[ℝ] tangentSpace I f x := (chartDifferential I f φ x).toLinearMap.codRestrict (tangentSpace I f x) (fun v => (chartTangentVector I f hf φ hφ x hx v).property) exact (LinearEquiv.ofBijective L ⟨fun v w h => chartDifferential_injective I f hf φ hφ x hx (congrArg val h), chartTangentVector_surjective I f hf φ hφ x hx⟩).toContinuousLinearEquiv
def secondFundamentalForm reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The second fundamental form of a C² Euclidean embedding at a point is the symmetric bilinear form on the full tangent space, with values in the normal space, whose value on the images of two model directions under any admissible chart parametrization is the orthogonal projection onto the normal space of the Hessian of that parametrization in those directions; the form is the same for every admissible chart.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
x :
M
def
secondFundamentalForm I f hf x :
tangentSpace I f x →L[ℝ] tangentSpace I f x →L[ℝ] normalSpace I f x
given by
choose (exists_secondFundamentalForm I f hf x)
theorem secondFundamentalForm_chart reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
A smooth Euclidean embedding f with embedding certificate hf, model with corners I, and an admissible chart φ at x with atlas and source conditions hφ and hx, and two model directions v and w, satisfies: the second fundamental form at x, evaluated on the tangent vectors that the chart differential assigns to v and w, equals the orthogonal projection onto the normal space of the chart Hessian applied to v and w.
Formal statement
hypotheses
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
x :
M
φ :
hφ :
φ ∈ maximalAtlas I 2 M
hx :
x ∈ φ.source
v w :
F
conclusion
secondFundamentalForm I f hf x (chartTangentVector I f hf φ hφ x hx v) (chartTangentVector I f hf φ hφ x hx w)
Proof (Lean source)
theorem secondFundamentalForm_chart (f : M → E)
(hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M)
(φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M)
(hx : x ∈ φ.source) (v w : F) :
secondFundamentalForm I f hf x (chartTangentVector I f hf φ hφ x hx v)
(chartTangentVector I f hf φ hφ x hx w) =
(normalSpace I f x).orthogonalProjectionOnto (chartHessian I f φ x v w) :=
(Classical.choose_spec (exists_secondFundamentalForm I f hf x)).2 φ hφ hx v w
def embeddingShapeOperator reviewed
⚑ flagged
Causalean.Mathlib.Geometry.Manifold.EmbeddedNormalGeometry
The extrinsic shape operator uses the full tangent metric and is indexed by a normal vector.
Definition (Lean source)
parameters
F :
Type u_1
E :
Type u_2
H :
Type u_3
M :
Type u_4
f :
M → E
hf :
IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f
x :
M
u :
normalSpace I f x
def
embeddingShapeOperator I f hf x u :
tangentSpace I f x →L[ℝ] tangentSpace I f x
given by
shapeOperator (secondFundamentalForm I f hf x) u
18 supporting declarations (lemmas, instances)
-
shapeOperator_innertheorem — The shape operator satisfies its defining inner-product identity.hypothesesT :sharedType u_1N :sharedType u_2B :T →L[ℝ] T →L[ℝ] Nu :Nv w :Tconclusion⟪shapeOperator B u v, w⟫_ℝ = ⟪u, B v w⟫_ℝProof (Lean source)
theorem shapeOperator_inner (B : T →L[ℝ] T →L[ℝ] N) (u : N) (v w : T) : ⟪shapeOperator B u v, w⟫_ℝ = ⟪u, B v w⟫_ℝ := by exact InnerProductSpace.continuousLinearMapOfBilin_apply _ _ _ -
shapeOperator_addtheorem — Shape operators depend additively on the indexing normal vector.hypothesesT :sharedType u_1N :sharedType u_2B :T →L[ℝ] T →L[ℝ] Nu z :NconclusionProof (Lean source)
theorem shapeOperator_add (B : T →L[ℝ] T →L[ℝ] N) (u z : N) : shapeOperator B (u + z) = shapeOperator B u + shapeOperator B z := by ext v apply ext_inner_right ℝ intro w simp [shapeOperator_inner, inner_add_left] -
shapeOperator_smultheorem — Shape operators depend linearly on real rescaling of the indexing normal vector.hypothesesT :sharedType u_1N :sharedType u_2B :T →L[ℝ] T →L[ℝ] Na :ℝu :NconclusionshapeOperator B (a • u) = a • shapeOperator B uProof (Lean source)
theorem shapeOperator_smul (B : T →L[ℝ] T →L[ℝ] N) (a : ℝ) (u : N) : shapeOperator B (a • u) = a • shapeOperator B u := by ext v apply ext_inner_right ℝ intro w simp [shapeOperator_inner, inner_smul_left] -
shapeOperator_selfAdjointtheorem — A symmetric normal-valued bilinear form gives self-adjoint shape operators.hypothesesT :sharedType u_1N :sharedType u_2B :T →L[ℝ] T →L[ℝ] NhB :∀ v w, B v w = B w vu :NconclusionIsSelfAdjoint (shapeOperator B u)Proof (Lean source)
theorem shapeOperator_selfAdjoint (B : T →L[ℝ] T →L[ℝ] N) (hB : ∀ v w, B v w = B w v) (u : N) : IsSelfAdjoint (shapeOperator B u) := by apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr intro v w change ⟪shapeOperator B u v, w⟫_ℝ = ⟪v, shapeOperator B u w⟫_ℝ rw [shapeOperator_inner, ← real_inner_comm v (shapeOperator B u w), shapeOperator_inner, hB v w] -
tubeDeterminant_eq_matrixtheorem — The tube determinant can be computed in any tangent basis without changing its value.hypothesesconclusiontubeDeterminant B a uProof (Lean source)
theorem tubeDeterminant_eq_matrix {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℝ T) (B : T →L[ℝ] T →L[ℝ] N) (a : ℝ) (u : N) : tubeDeterminant B a u = det (toMatrix b b (id - a • (shapeOperator B u).toLinearMap)) := by exact (LinearMap.det_toMatrix b _).symm -
tubeDeterminant_zerotheorem — The tube determinant equals one at zero displacement.hypothesesT :sharedType u_1N :sharedType u_2B :T →L[ℝ] T →L[ℝ] Nu :NconclusiontubeDeterminant B 0 u = 1Proof (Lean source)
theorem tubeDeterminant_zero (B : T →L[ℝ] T →L[ℝ] N) (u : N) : tubeDeterminant B 0 u = 1 := by simp [tubeDeterminant] -
extendedChart_target_subset_closure_interiortheorem — Every extended chart target is contained in the closure of its interior, including its boundary points.hypothesesF :sharedType u_1H :sharedType u_3M :sharedType u_4φ :Proof (Lean source)
theorem extendedChart_target_subset_closure_interior (φ : OpenPartialHomeomorph M H) : (φ.extend I).target ⊆ closure (interior (φ.extend I).target) := by intro y hy have ho : IsOpen (I.symm ⁻¹' φ.target) := φ.open_target.preimage I.continuous_symm have hy' : y ∈ I.symm ⁻¹' φ.target ∩ range I := by simpa only [φ.extend_target] using hy rw [mem_closure_iff_nhds] intro t ht obtain ⟨z, ⟨hzt, hzo⟩, hzi⟩ := mem_closure_iff_nhds.mp (I.range_subset_closure_interior hy'.2) _ (Filter.inter_mem ht (ho.mem_nhds hy'.1)) refine ⟨z, hzt, ?_⟩ rw [φ.extend_target, interior_inter, ho.interior_eq] exact ⟨hzo, hzi⟩ -
contDiffOn_chartParametrizationtheorem — Composing a C² embedding with an admissible inverse extended chart gives a C² parametrization on the full chart target.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ :hφ :φ ∈ maximalAtlas I 2 MconclusionContDiffOn ℝ 2 (f ∘ (φ.extend I).symm) (φ.extend I).targetProof (Lean source)
theorem contDiffOn_chartParametrization (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) : ContDiffOn ℝ 2 (f ∘ (φ.extend I).symm) (φ.extend I).target := by apply ContMDiffOn.contDiffOn rw [φ.extend_target'] exact hf.contMDiff.comp_contMDiffOn (contMDiffOn_extend_symm hφ) -
chartHessian_symmetrictheorem — Admissible C² local parametrizations have symmetric Hessians at every chart point.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ :hφ :φ ∈ maximalAtlas I 2 Mx :Mhx :x ∈ φ.sourcev w :FconclusionchartHessian I f φ x v w = chartHessian I f φ x w vProof (Lean source)
theorem chartHessian_symmetric (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (x : M) (hx : x ∈ φ.source) (v w : F) : chartHessian I f φ x v w = chartHessian I f φ x w v := by have hx' : x ∈ (φ.extend I).source := by simpa using hx have hy := (φ.extend I).map_source hx' have hu : UniqueDiffOn ℝ (φ.extend I).target := by rw [φ.extend_target] exact I.uniqueDiffOn_preimage φ.open_target exact ((contDiffOn_chartParametrization I f hf φ hφ _ hy).isSymmSndFDerivWithinAt (by simp) hu (extendedChart_target_subset_closure_interior I φ hy) hy) v w -
chartHessian_changetheorem — The Hessian chart-change law has exactly one additional tangent-valued first-derivative term.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ ψ :hφ :φ ∈ maximalAtlas I 2 Mhψ :ψ ∈ maximalAtlas I 2 Mx :Mhxφ :x ∈ φ.sourcehxψ :x ∈ ψ.sourcev w :Fconclusionq :(φ.extend I) ∘ (ψ.extend I).symms :(ψ.extend I).targety :(ψ.extend I) xD :fderivWithin ℝ q s yHq :fderivWithin ℝ (fun z => fderivWithin ℝ q s z) s ychartHessian I f ψ x v w= chartHessian I f φ x (D v) (D w) + chartDifferential I f φ x (Hq v w)Proof (Lean source)
theorem chartHessian_change (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ ψ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (hψ : ψ ∈ maximalAtlas I 2 M) (x : M) (hxφ : x ∈ φ.source) (hxψ : x ∈ ψ.source) (v w : F) : let q := (φ.extend I) ∘ (ψ.extend I).symm let s := (ψ.extend I).target let y := (ψ.extend I) x let D := fderivWithin ℝ q s y let Hq := fderivWithin ℝ (fun z => fderivWithin ℝ q s z) s y chartHessian I f ψ x v w = chartHessian I f φ x (D v) (D w) + chartDifferential I f φ x (Hq v w) := by let q := (φ.extend I) ∘ (ψ.extend I).symm let s := (ψ.extend I).target let t := (φ.extend I).target let y := (ψ.extend I) x let g := f ∘ (φ.extend I).symm let p := f ∘ (ψ.extend I).symm have hxψ' : x ∈ (ψ.extend I).source := by simpa using hxψ have hxφ' : x ∈ (φ.extend I).source := by simpa using hxφ have hy : y ∈ s := (ψ.extend I).map_source hxψ' have hqy : q y = (φ.extend I) x := by dsimp only [q, y, Function.comp_apply]; rw [(ψ.extend I).left_inv hxψ'] have hqt : q y ∈ t := hqy ▸ (φ.extend I).map_source hxφ' have hs : UniqueDiffOn ℝ s := by dsimp only [s]; rw [ψ.extend_target]; exact I.uniqueDiffOn_preimage ψ.open_target have ht : UniqueDiffOn ℝ t := by dsimp only [t]; rw [φ.extend_target]; exact I.uniqueDiffOn_preimage φ.open_target obtain ⟨hq, hmap, _⟩ := chart_transition_data I f φ ψ hφ hψ x hxφ hxψ have hdq := hq.differentiableWithinAt (by norm_num) have hqder : DifferentiableWithinAt ℝ (fderivWithin ℝ q s) s y := (hq.fderivWithin_right hs (m := 1) (by norm_num) hy).differentiableWithinAt (by norm_num) have hg : ContDiffOn ℝ 2 g t := contDiffOn_chartParametrization I f hf φ hφ have hgder := ((hg.fderivWithin ht (m := 1) (by norm_num)).differentiableOn (by norm_num) (q y) hqt).hasFDerivWithinAt have hto := tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within q hdq.continuousWithinAt hmap have houter := hgder.comp_of_tendsto y hdq.hasFDerivWithinAt hto have hc := houter.clm_comp hqder.hasFDerivWithinAt have heq : fderivWithin ℝ p s =ᶠ[𝓝[s] y] (fun z => (fderivWithin ℝ g t (q z)).comp (fderivWithin ℝ q s z)) := by have hlocal : ∀ᶠ z in 𝓝[s] y, (ψ.extend I).symm z ∈ φ.source := (ψ.continuousAt_extend_symm (I := I) hxψ).continuousWithinAt.preimage_mem_nhdsWithin (φ.open_source.mem_nhds (by simpa only [(ψ.extend I).left_inv hxψ'] using hxφ)) filter_upwards [hlocal, self_mem_nhdsWithin] with z hz hzs have hzψ : (ψ.extend I).symm z ∈ ψ.source := by simpa using (ψ.extend I).map_target hzs have hid := chartDifferential_change I f hf φ ψ hφ hψ ((ψ.extend I).symm z) hz hzψ simpa only [chartDifferential, (ψ.extend I).right_inv hzs, q, s, t, g, p, Function.comp_apply] using hid have hder := (hc.congr_of_eventuallyEq heq (heq.self_of_nhdsWithin hy)).fderivWithin (hs y hy) have happ := congrArg (fun L : F →L[ℝ] F →L[ℝ] E => L v w) hder change fderivWithin ℝ (fderivWithin ℝ p s) s y v w = fderivWithin ℝ (fderivWithin ℝ g t) t ((φ.extend I) x) (fderivWithin ℝ q s y v) (fderivWithin ℝ q s y w) + fderivWithin ℝ g t ((φ.extend I) x) (fderivWithin ℝ (fderivWithin ℝ q s) s y v w) simpa only [add_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.compL_apply, ContinuousLinearMap.flip_apply, Function.comp_apply, hqy, add_comm] using happ -
chart_normalHessian_congrtheorem — Normal projection of the Hessian depends only on the two ambient tangent vectors, not on the chart.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ ψ :hφ :φ ∈ maximalAtlas I 2 Mhψ :ψ ∈ maximalAtlas I 2 Mx :Mhxφ :x ∈ φ.sourcehxψ :x ∈ ψ.sourcev w v' w' :Fhv :chartDifferential I f φ x v = chartDifferential I f ψ x v'hw :chartDifferential I f φ x w = chartDifferential I f ψ x w'conclusionProof (Lean source)
theorem chart_normalHessian_congr (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ ψ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (hψ : ψ ∈ maximalAtlas I 2 M) (x : M) (hxφ : x ∈ φ.source) (hxψ : x ∈ ψ.source) (v w v' w' : F) (hv : chartDifferential I f φ x v = chartDifferential I f ψ x v') (hw : chartDifferential I f φ x w = chartDifferential I f ψ x w') : (normalSpace I f x).orthogonalProjectionOnto (chartHessian I f φ x v w) = (normalSpace I f x).orthogonalProjectionOnto (chartHessian I f ψ x v' w') := by let q := (φ.extend I) ∘ (ψ.extend I).symm let s := (ψ.extend I).target let y := (ψ.extend I) x let D := fderivWithin ℝ q s y have hD := chartDifferential_change I f hf φ ψ hφ hψ x hxφ hxψ have hvD : v = D v' := by apply chartDifferential_injective I f hf φ hφ x hxφ rw [hv, hD] rfl have hwD : w = D w' := by apply chartDifferential_injective I f hf φ hφ x hxφ rw [hw, hD] rfl have hchange := chartHessian_change I f hf φ ψ hφ hψ x hxφ hxψ v' w' dsimp only at hchange rw [← hvD, ← hwD] at hchange rw [hchange, map_add] have hzero : (normalSpace I f x).orthogonalProjectionOnto (chartDifferential I f φ x (fderivWithin ℝ (fderivWithin ℝ q s) s y v' w')) = 0 := by apply Submodule.orthogonalProjectionOnto_eq_zero_iff.mpr rw [normalSpace, Submodule.orthogonal_orthogonal, ← chartDifferential_range I f hf φ hφ x hxφ] exact ⟨_, rfl⟩ rw [hzero, add_zero] -
chartTangentVector_surjectivetheorem — Every full tangent vector is represented by a model vector in any admissible chart.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ :hφ :φ ∈ maximalAtlas I 2 Mx :Mhx :x ∈ φ.sourceconclusionSurjective (chartTangentVector I f hf φ hφ x hx)Proof (Lean source)
theorem chartTangentVector_surjective (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (x : M) (hx : x ∈ φ.source) : Surjective (chartTangentVector I f hf φ hφ x hx) := by intro v have hv : (v : E) ∈ (chartDifferential I f φ x).toLinearMap.range := by simpa only [chartDifferential_range I f hf φ hφ x hx] using v.property obtain ⟨w, hw⟩ := hv exact ⟨w, Subtype.ext hw⟩ -
chartTangentEquiv_applytheorem — The chart tangent equivalence applies the parametrization differential.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fφ :hφ :φ ∈ maximalAtlas I 2 Mx :Mhx :x ∈ φ.sourcev :FconclusionchartTangentEquiv I f hf φ hφ x hx v = chartTangentVector I f hf φ hφ x hx vProof (Lean source)
theorem chartTangentEquiv_apply (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (x : M) (hx : x ∈ φ.source) (v : F) : chartTangentEquiv I f hf φ hφ x hx v = chartTangentVector I f hf φ hφ x hx v := rfl -
exists_secondFundamentalFormtheorem — A symmetric normal-valued bilinear form simultaneously represents the Hessian in every admissible chart.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :Mconclusion∃ B : tangentSpace I f x →L[ℝ] tangentSpace I f x →L[ℝ] normalSpace I f x,conclusion 1v w :B v w = B w vconclusion 2B (chartTangentVector I f hf φ hφ x hx v) (chartTangentVector I f hf φ hφ x hx w)Proof (Lean source)
theorem exists_secondFundamentalForm (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) : ∃ B : tangentSpace I f x →L[ℝ] tangentSpace I f x →L[ℝ] normalSpace I f x, (∀ v w, B v w = B w v) ∧ ∀ (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (hx : x ∈ φ.source) (v w : F), B (chartTangentVector I f hf φ hφ x hx v) (chartTangentVector I f hf φ hφ x hx w) = (normalSpace I f x).orthogonalProjectionOnto (chartHessian I f φ x v w) := by let φ := chartAt H x have hφ : φ ∈ maximalAtlas I 2 M := IsManifold.chart_mem_maximalAtlas x have hx : x ∈ φ.source := mem_chart_source H x let e := chartTangentEquiv I f hf φ hφ x hx let H := (chartHessian I f φ x).bilinearComp e.symm.toContinuousLinearMap e.symm.toContinuousLinearMap let B := ((normalSpace I f x).orthogonalProjectionOnto.postcomp (tangentSpace I f x)).comp H refine ⟨B, ?_, ?_⟩ · intro v w change (normalSpace I f x).orthogonalProjectionOnto (chartHessian I f φ x (e.symm v) (e.symm w)) = _ rw [chartHessian_symmetric I f hf φ hφ x hx] rfl · intro ψ hψ hxψ v w change (normalSpace I f x).orthogonalProjectionOnto (chartHessian I f φ x (e.symm (chartTangentVector I f hf ψ hψ x hxψ v)) (e.symm (chartTangentVector I f hf ψ hψ x hxψ w))) = _ apply chart_normalHessian_congr I f hf φ ψ hφ hψ x hx hxψ · exact congrArg val (e.apply_symm_apply _) · exact congrArg val (e.apply_symm_apply _) -
secondFundamentalForm_symmetrictheorem — The second fundamental form is symmetric in its full tangent arguments.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :Mv w :tangentSpace I f xconclusionsecondFundamentalForm I f hf x v w = secondFundamentalForm I f hf x w vProof (Lean source)
theorem secondFundamentalForm_symmetric (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) (v w : tangentSpace I f x) : secondFundamentalForm I f hf x v w = secondFundamentalForm I f hf x w v := (Classical.choose_spec (exists_secondFundamentalForm I f hf x)).1 v w -
secondFundamentalForm_uniquetheorem — Any bilinear form representing all chart normal Hessians equals the second fundamental form.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :MB :tangentSpace I f x →L[ℝ] tangentSpace I f x →L[ℝ] normalSpace I f xhB :∀ (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (hx : x ∈ φ.source) (v w : F),B (chartTangentVector I f hf φ hφ x hx v) (chartTangentVector I f hf φ hφ x hx w)conclusionB = secondFundamentalForm I f hf xProof (Lean source)
theorem secondFundamentalForm_unique (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) (B : tangentSpace I f x →L[ℝ] tangentSpace I f x →L[ℝ] normalSpace I f x) (hB : ∀ (φ : OpenPartialHomeomorph M H) (hφ : φ ∈ maximalAtlas I 2 M) (hx : x ∈ φ.source) (v w : F), B (chartTangentVector I f hf φ hφ x hx v) (chartTangentVector I f hf φ hφ x hx w) = (normalSpace I f x).orthogonalProjectionOnto (chartHessian I f φ x v w)) : B = secondFundamentalForm I f hf x := by let φ := chartAt H x have hφ : φ ∈ maximalAtlas I 2 M := IsManifold.chart_mem_maximalAtlas x have hx : x ∈ φ.source := mem_chart_source H x apply ContinuousLinearMap.ext intro v apply ContinuousLinearMap.ext intro w obtain ⟨v', rfl⟩ := chartTangentVector_surjective I f hf φ hφ x hx v obtain ⟨w', rfl⟩ := chartTangentVector_surjective I f hf φ hφ x hx w exact (hB φ hφ hx v' w').trans (secondFundamentalForm_chart I f hf x φ hφ hx v' w').symm -
embeddingShapeOperator_innertheorem — The extrinsic shape operator satisfies the geometric inner-product identity.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :Mu :normalSpace I f xv w :tangentSpace I f xconclusion⟪embeddingShapeOperator I f hf x u v, w⟫_ℝ = ⟪u, secondFundamentalForm I f hf x v w⟫_ℝProof (Lean source)
theorem embeddingShapeOperator_inner (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) (u : normalSpace I f x) (v w : tangentSpace I f x) : ⟪embeddingShapeOperator I f hf x u v, w⟫_ℝ = ⟪u, secondFundamentalForm I f hf x v w⟫_ℝ := shapeOperator_inner _ _ _ _ -
embeddingShapeOperator_selfAdjointtheorem — Every extrinsic shape operator is self-adjoint, including at boundary points.hypothesesF :sharedType u_1E :sharedType u_2H :sharedType u_3M :sharedType u_4f :M → Ehf :IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 fx :Mu :normalSpace I f xconclusionIsSelfAdjoint (embeddingShapeOperator I f hf x u)Proof (Lean source)
theorem embeddingShapeOperator_selfAdjoint (f : M → E) (hf : IsSmoothEmbedding I (modelWithCornersSelf ℝ E) 2 f) (x : M) (u : normalSpace I f x) : IsSelfAdjoint (embeddingShapeOperator I f hf x u) := shapeOperator_selfAdjoint _ (secondFundamentalForm_symmetric I f hf x) u