HarmonicLevelStep.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One quantitative step of the harmonic level-set iteration

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_level_step line 19

Source documentation

The same constants work for every nested pair of interior balls and every pair of nonnegative levels.

theorem NoncollapsedRCD.harmonic_level_step {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ p C : ℝ, 2 < p ∧ 0 < C ∧ ∀ (x : X) (R : ℝ), 0 < R → -1 ≤ K*R^2 →
      ∀ u : SobolevSpace (hausdorff n X) hX.quadratic,
      IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball x R) u →
      ∀ r s k h : ℝ, 0 ≤ r → r < s → s < R → 0 ≤ k → k < h →
      let U := SobolevSpace.toLp (hausdorff n X) hX.quadratic u
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.toLp