HarmonicAffineNondegeneracy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Value nondegeneracy of the actual centered harmonic coordinates

theorem OAI.RegularPointCoordinates.harmonic_affine_nondegeneracy line 19

Source documentation

The constant and the coefficient in the exact energy frame are both controlled by the value norm of one affine function. This follows from the published harmonic gradient and mean-value inputs already in use.

theorem 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