OAI/Geometry/RCD/Harmonic/EuclideanHarmonicContraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A single strict affine contraction for all normalized harmonic models

  1. theorem OAI.RegularPointCoordinates.EuclideanHarmonicHessianInput.affine_contraction line 15

    Source documentation

    The Euclidean derivative estimate chooses the dyadic scale before any harmonic function, working radius, or RCD sequence is chosen.

    theorem EuclideanHarmonicHessianInput.affine_contraction {n : ℕ}
    (hinput : EuclideanHarmonicHessianInput n) :
    ∃ m : ℕ, 3 ≤ m ∧ ∀ S : ℝ, 0 < S →
      let θ := (1 / 2 : ℝ) ^ m
…

    Mentions: OAI.RegularPointCoordinates.EuclideanHarmonicHessianInput