OAI/Analysis/AffineBernstein/ProductAreaChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.affineEpigraph_product_area_chart line 25

   Source documentation

   Actual graph-area change of variables in a full flat projective chart, expressed in the true product Haar measure on base times angular plane.

   theorem affineEpigraph_product_area_chart {n : ℕ} {Ω : Set (Space n)}
       (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
       {D : Set S} (hD : IsOpen D)
       (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       (hzero : ∀ s ∈ D, (0:E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       (bS : OrthonormalBasis ι ℝ S) (bF : OrthonormalBasis κ ℝ F)
       (f : WithLp 2 (F × ℝ) ≃ₗᵢ[ℝ] E) (e : Fin n ≃ ι ⊕ κ) :
       let Z := flatProductCoordinates bS bF e
   …

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