FlatChartInjective.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.affineEpigraph_gaussPoint_injective_flat line 17

Source comment

Flat normalization removes exactly the radial ambiguity of the actual Gauss inverse. This is global on each compact positive fiber.

theorem affineEpigraph_gaussPoint_injective_flat {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 × ℝ))
    {B : Set S} (hB : IsOpen B)
    (hK : ∀ s ∈ B, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ B, (0 : E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    {s : S} (hs : s ∈ B) {e₁ e₂ d : E}
    (h₁ : inner ℝ e₁ d = 1) (h₂ : inner ℝ e₂ d = 1)
    (he : gaussPoint {y | (s,y) ∈ affineEpigraphPullback Ω u a L} e₁ =
      gaussPoint {y | (s,y) ∈ affineEpigraphPullback Ω u a L} e₂) : e₁ = e₂ := by
…

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

theorem OAI.AffineBernstein.affineEpigraph_flat_graph_injective line 43

Source comment

The flat support parametrization is globally one-to-one after projection to the original graph domain, not merely a local immersion.

theorem affineEpigraph_flat_graph_injective {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 × ℝ))
    {B : Set S} (hB : IsOpen B)
    (hK : ∀ s ∈ B, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ B, (0 : E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
    (q₀ : S × E) (d : E) (hd : inner ℝ q₀.2 d = 1)
    (J : Space n →L[ℝ] (S × E)) (hi : Function.Injective J)
    (hJ : ∀ v, inner ℝ (J v).2 d = 0) :
    let Y := fun q : S × E => gaussPoint {y | (q.1,y) ∈ affineEpigraphPullback Ω u a L} q.2
…

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