LevelRecursion

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Chebyshev level bound and the recursion assembly

Two purely analytic helpers used by the generic De Giorgi core (Stampacchia/DeGiorgiCore.lean):

• real_chebyshev_level: the real-valued Chebyshev/Markov inequality ε · (μ S)^{1/p} ≤ ‖h‖_{L^p} whenever S ⊆ {ε ≤ h} and ‖h‖_{L^p} < ∞.
• sq_level_recursion_of_le: the elementary squaring/superadditivity step turning ε · |A_l|^{1/p} ≤ R into ε² · |A_l|^{2/p} ≤ R², combined with the subadditivity (a+b)^{γ} ≤ a^{γ} + b^{γ} for the two-copy volume.

Both are proved at default heartbeats, no sorry.

theorem HCPolySupport.real_chebyshev_level {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} (hp0 : p ≠ 0) (hptop : p ≠ ⊤) {h : α → ℝ} (hfin : MeasureTheory.eLpNorm h p μ ≠ ⊤) {ε : ℝ} (hε : 0 ≤ ε) {S : Set α} (hSsub : ∀ x ∈ S, ε ≤ h x) : ε * (μ S).toReal ^ (1 / p.toReal) ≤ (MeasureTheory.eLpNorm h p μ).toReal

Real Chebyshev level bound. If S ⊆ {x | ε ≤ h x} with ε ≥ 0 and ‖h‖_{L^p(μ)} < ∞, then ε · (μ S)^{1/p} ≤ ‖h‖_{L^p(μ)} in real numbers.

theorem HCPolySupport.sq_level_recursion_of_le {ε r a b N₁ N₂ R : ℝ} (hε : 0 ≤ ε) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (ha : 0 ≤ a) (hb : 0 ≤ b) (hN₁ : ε * a ^ r ≤ N₁) (hN₂ : ε * b ^ r ≤ N₂) (hsum : N₁ + N₂ ≤ R) (hR : 0 ≤ R) : ε ^ 2 * (a + b) ^ (2 * r) ≤ R ^ 2

Squaring step of the level recursion. From the two per-copy Chebyshev bounds ε · (vol S₁)^{1/p} ≤ N₁, ε · (vol S₂)^{1/p} ≤ N₂ and a bound N₁ + N₂ ≤ R, together with 0 ≤ ε and 0 < 1/p ≤ 1, we obtain ε² · (vol S₁ + vol S₂)^{2/p} ≤ R².