HarmonicAffineImprovement.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform affine improvement from published harmonic compactness

The threshold is uniform in the center, radius, coordinates and harmonic function. All inputs are measured approximation, a rescaled curvature bound, harmonicity and an actual normalized L² bound. The affine estimate itself is proved by a compactness contradiction.

def OAI.RegularPointCoordinates.harmonicTargetNorm line 22
Source documentation
The averaged norm, with its radius dependence exposed for rescaling.
```
def harmonicTargetNorm {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (p : X) (r : ℝ) (w : SobolevSpace (hausdorff n X) hX.quadratic) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff
def OAI.RegularPointCoordinates.harmonicAffineResidualNorm line 29
Source documentation
The averaged affine residual, with its radius dependence exposed.
```
def harmonicAffineResidualNorm {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    (u : Fin n → SobolevSpace (hausdorff n X) hX.quadratic)
    (p : X) (r : ℝ) (w : SobolevSpace (hausdorff n X) hX.quadratic) : ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff
structure OAI.RegularPointCoordinates.NormalizedHarmonicTest line 39
Source documentation
One normalized harmonic test on a measured almost-Euclidean ball.
```
structure NormalizedHarmonicTest {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (S ε : ℝ) where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
def OAI.RegularPointCoordinates.NormalizedHarmonicTest.residualNorm line 58
theorem OAI.RegularPointCoordinates.harmonic_affine_improvement_of_measured_approximation line 67
Source documentation
The quantitative affine-improvement theorem for normalized harmonic functions. There is no energy-bound or affine-fit premise: the former is derived from Jiang's estimate and the latter from the Euclidean limit.
```
theorem harmonic_affine_improvement_of_measured_approximation
    {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n)
    (hcompact : LocalHarmonicMomentCompactnessInput hX)
    (hgradient : LocalHarmonicL2GradientInput hX)
    (heuclidean : EuclideanHarmonicHessianInput n) :
    ∃ m : ℕ, 3 ≤ m ∧ ∀ S : ℝ, 0 < S →
      ∃ ε : ℝ, 0 < ε ∧ ∀ d : NormalizedHarmonicTest hX S ε,
        d.residualNorm ((1 / 2 : ℝ) ^ m * S) <
          (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ m * Real.sqrt ((1 / 2 : ℝ) ^ m) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicMomentCompactnessInput, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.EuclideanHarmonicHessianInput, OAI.RegularPointCoordinates.NormalizedHarmonicTest