ScaledHarmonicAffine.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Radius-weighted affine coefficients in centered harmonic coordinates

theorem OAI.RegularPointCoordinates.scaled_harmonic_affine_nondegeneracy line 18

Source documentation

Weighting the exact-frame coefficient by the physical radius gives one affine nondegeneracy constant at every positive scale. The constant coefficient retains its unweighted normalization.

theorem scaled_harmonic_affine_nondegeneracy {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
    (hgradient : LocalHarmonicL2GradientInput hX) (hmean : LocalHarmonicL2MeanValueInput hX)
    (hn : 2 ≤ n) {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ Cg Cm : ℝ, 1 ≤ Cg ∧ 1 ≤ Cm ∧
      ∀ (p : X) (R : ℝ), 0 < R → -κ ≤ K * R ^ 2 →
      ∀ (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic) (V : X → Euclidean n),
      (∀ j, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p R) (u j)) →
      ContinuousOn V (ball p R) → V p = 0 →
      (∀ j, SobolevSpace.toLp (hausdorff n X) hX.quadratic (u j) =ᵐ[
        (hausdorff n X).restrict (ball p R)] fun x => V x j) →
      ∀ (N : Euclidean n ≃L[ℝ] Euclidean n),
      IsExactMeanNormalization (hausdorff n X) hX.quadratic
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.LocalHarmonicL2MeanValueInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.IsExactMeanNormalization