SectionNormalizationFamily.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.centered_section_normalization_family line 22

Source documentation

The actual uniform, zero-preserving section normalizations in rigidity.tex. The radius is fixed before height; the maps are produced from the compact convex sections and their genuine balance inclusion.

theorem centered_section_normalization_family {n : ℕ} (hn : 1 ≤ n)
    {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
    (hzero : u 0=0) (hdzero : fderiv ℝ u 0=0)
    {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ t : ℝ, 0 < t → ∃ A : Space n ≃L[ℝ] Space n,
      Metric.ball 0 1 ⊆ tangentSection univ (normalizedFunction u A t) 0 1 ∧
      tangentSection univ (normalizedFunction u A t) 0 1 ⊆ Metric.ball 0 R := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.tangentSection, OAI.AffineBernstein.normalizedFunction