OAI/Analysis/AffineBernstein/NormalizedSigmaTransport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineEpigraphPullback_normalize line 15
2. theorem OAI.AffineBernstein.affineEpigraph_sigma_normalization line 30

   Source documentation

   Actual sigma in any diagonal-base/transverse GL normalization. All support smoothness and determinant positivity are produced by the positive Hessian of the original graph, not assumed as sigma identities.

   theorem affineEpigraph_sigma_normalization {n k m d : ℕ} (hm : 1 ≤ m)
       (hn : n = k+d) (bE : OrthonormalBasis (Fin d ⊕ Unit) ℝ (Space m))
       {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (a : Space n × ℝ) (L : (Space k × Space m) ≃L[ℝ] (Space n × ℝ))
       (B : Space k ≃L[ℝ] Space k) (A : Space m ≃L[ℝ] Space m)
       (coeff : Fin k → ℝ) (hcoeff : ∀ i, coeff i ≠ 0) (hB : ∀ s i, B s i = coeff i*s i)
       {D : Set (Space k)} (hD : IsOpen D)
       {Q : Set (Space k)} (hQ : MeasurableSet Q) (hQD : B '' Q ⊆ D)
       (hs : ∀ s ∈ Q, ∀ i, s i ≠ 0)
       (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈
         affineEpigraphPullback Ω u a ((B.prodCongr A).symm.trans L)})
   …

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