OAI/Analysis/AffineBernstein/ActualChartArea.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.graph_chart_parametricAreaDensity line 16

   Source comment

   The actual graph area in an arbitrary smooth chart, with arbitrary inward normalized conormal. This is a density identity, not a stationarity premise.

   lemma graph_chart_parametricAreaDensity {n : ℕ} {Ω U : Set (Space n)}
       (hΩ : IsOpen Ω) (hU : IsOpen U) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       {φ : Space n → Space n} (hφ : ContDiffOn ℝ ∞ φ U) (hφΩ : φ '' U ⊆ Ω)
       {x : Space n} (hx : x ∈ U) (hJ : (parametricJacobian φ x).det ≠ 0)
       (ν : (Space n × ℝ) →L[ℝ] ℝ) (ξ : Space n × ℝ)
       (hν : ν.comp (fderiv ℝ (fun y => (φ y,u (φ y))) x) = 0)
       (hξ : ν ξ = 1) (hc : 0 < ν ((0 : Space n),1)) :
       parametricAreaDensity (graphAmbientBasis n) (fun y => (φ y,u (φ y))) ν ξ x =
         |LinearMap.det (fderiv ℝ φ x).toLinearMap| * affineAreaDensity u (φ x) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.parametricJacobian, OAI.AffineBernstein.parametricAreaDensity, OAI.AffineBernstein.graphAmbientBasis, OAI.AffineBernstein.affineAreaDensity

2. theorem OAI.AffineBernstein.immersed_graph_local_area_transport line 52

   Source comment

   Exact local area transport for an arbitrary immersed parametrization of the actual graph. The inverse chart is constructed, and all measurable subsets of its source share the same determinant-normalized area identity.

   theorem immersed_graph_local_area_transport {E : Type*}
       [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {U Ω : Set (Space n)}
       (hU : IsOpen U) (hΩ : IsOpen Ω) {X : Space n → E} {u : Space n → ℝ}
       (hX : ContDiffOn ℝ ∞ X U) (hu : ContDiffOn ℝ ∞ u Ω)
       (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (a : Space n × ℝ) (L : E ≃L[ℝ] (Space n × ℝ))
       (him : ∀ y ∈ U, (a+L (X y)).1 ∈ Ω ∧ (a+L (X y)).2 = u (a+L (X y)).1)
       {x₀ : Space n} (hx₀ : x₀ ∈ U) (hi : Function.Injective (fderiv ℝ X x₀))
       (b : Module.Basis (Fin n ⊕ Unit) ℝ E) :
       ∃ φ : OpenPartialHomeomorph (Space n) (Space n), x₀ ∈ φ.source ∧ φ.source ⊆ U ∧
         φ.target ⊆ Ω ∧ ContDiffOn ℝ ∞ φ φ.source ∧ ContDiffOn ℝ ∞ φ.symm φ.target ∧
         (∀ x ∈ φ.source, a+L (X x) = (φ x,u (φ x))) ∧
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian