OAI/Analysis/AffineBernstein/LinearizedNormalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.inverseHessianTrace_eq_matrixTrace line 17
2. lemma OAI.AffineBernstein.contDiff_comp_cle line 23
3. lemma OAI.AffineBernstein.hessian_comp_cle line 27
4. lemma OAI.AffineBernstein.inverseHessianTrace_normalized_comp line 33
5. theorem OAI.AffineBernstein.centered_normalization_at_points line 46

   Source documentation

   The previously produced normalizations can put any finite collection of fixed original points in the same small inner ball.

   theorem centered_normalization_at_points {n : ℕ} (hn : 1 ≤ n)
       {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
       (hm : AffineMaximalOn univ u) (hzero : u 0=0) (hdzero : fderiv ℝ u 0=0)
       {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ) :
       ∃ R : ℝ, 1 ≤ R ∧ ∀ P : Finset (Space n),
         ∃ t : ℝ, 0 < t ∧ ∃ A : Space n ≃L[ℝ] Space n,
           BalancedNormalized ρ R (normalizedFunction u A t) ∧
           ∀ x ∈ P, A.symm x ∈ Metric.ball (0:Space n) (1/64:ℝ) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.BalancedNormalized, OAI.AffineBernstein.normalizedFunction