EnnrealShell

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The ℝ≥0∞ shell of the harmonic-approximation clauses

The frozen §4.3 anchor states both of its clauses in ℝ≥0∞: an indicator on the good event on the left, and ENNReal.ofReal-scalars multiplying ℝ≥0∞-valued norm carriers on the right. This module is the (analysis-free) bridge between the two, in three atoms:

• ofReal_mul_toReal_le — the product regrouping ofReal (c * X.toReal) ≤ ofReal c * X, valid at X = ⊤ as well (there the left side collapses to 0), so that no finiteness hypothesis on the right-hand carriers is ever needed;
• le_ofReal_mul_add_ofReal_mul — the two-summand shell: a real inequality between toReal values plus finiteness of the left side gives the frozen ℝ≥0∞ inequality;
• indicator_le_of_mem — the indicator collapse on the good event.

The fourth atom, eLpNorm_ne_top_of_eq_h10, supplies the one finiteness fact the shell does need: the anchor's left-hand side is ‖u - v‖_{L²(x+□_n)} and the anchor's own binders give u - v = w for an H¹₀(x+□_n) witness w, whose L² datum is part of its type.

No mathematics of the manuscript enters here; nothing in this file knows what a good event, a coefficient field or a scale is.

References

• ABK26, l.harmonic.approximation.good.scales, (the two clauses whose ℝ≥0∞ shape is targeted).

1. The ofReal-product regrouping

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ofReal_mul_toReal_le {c : ℝ} (hc : 0 ≤ c) (X : ENNReal) : ENNReal.ofReal (c * X.toReal) ≤ ENNReal.ofReal c * X

The product regrouping. Pushing a nonnegative real scalar through a toReal never increases the value, including at X = ⊤, where the left-hand side collapses to 0 while the right-hand side is 0 or ⊤.

This is what makes the shell free of finiteness hypotheses on the right-hand carriers: the frozen theorem's [g]_{H^s} and ‖∇h‖_{L²} legs are never known to be finite (the anchor's clause (iv) gives MemLp of the kernel, on □_m, not on the intersected window).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.le_ofReal_mul_add_ofReal_mul {A X Y : ENNReal} {c₁ c₂ : ℝ} (hA : A ≠ ⊤) (hc₁ : 0 ≤ c₁) (hc₂ : 0 ≤ c₂) (h : A.toReal ≤ c₁ * X.toReal + c₂ * Y.toReal) : A ≤ ENNReal.ofReal c₁ * X + ENNReal.ofReal c₂ * Y

The two-summand shell.

From a real inequality between toReal values, plus finiteness of the left-hand side alone, to the frozen theorem's ℝ≥0∞ shape A ≤ ofReal c₁ * X + ofReal c₂ * Y.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.le_ofReal_mul_bracket_add_three {A X Y Z W : ENNReal} {c₁ b c₂ c₃ c₄ : ℝ} (hA : A ≠ ⊤) (hc₁ : 0 ≤ c₁) (hb : 0 ≤ b) (hc₂ : 0 ≤ c₂) (hc₃ : 0 ≤ c₃) (hc₄ : 0 ≤ c₄) (h : A.toReal ≤ c₁ * (X.toReal + b) + c₂ * Y.toReal + c₃ * Z.toReal + c₄ * W.toReal) : A ≤ ENNReal.ofReal c₁ * (X + ENNReal.ofReal b) + ENNReal.ofReal c₂ * Y + ENNReal.ofReal c₃ * Z + ENNReal.ofReal c₄ * W

The four-summand shell with the in-bracket companion.

The frozen theorem's general clause has the shape `ofReal c₁ * (X + ofReal b)

• ofReal c₂ * Y + ofReal c₃ * Z + ofReal c₄ * W, the companion b` sitting inside the bracket with no constant of its own. Same principle as the two-summand shell: only the left-hand side must be finite.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.two_summand_coeff_mono {a a' b b' : ℝ} {X Y : ENNReal} (ha : a ≤ a') (hb : b ≤ b') : ENNReal.ofReal a * X + ENNReal.ofReal b * Y ≤ ENNReal.ofReal a' * X + ENNReal.ofReal b' * Y

Constant monotonicity of a two-summand ℝ≥0∞ right-hand side. Used to raise a clause proved at one constant to the joint constant of the assembly, without ever writing the (large) carriers out.

2. The indicator collapse

theorem Algsuperdiff.Section4.Provider.ExcessDecay.indicator_le_of_mem {α : Type u_1} {G : Set α} {f : α → ENNReal} {R : ENNReal} {omega : α} (h : omega ∈ G → f omega ≤ R) : G.indicator f omega ≤ R

The indicator collapse on the good event. Off the event the indicator is 0; on it, the estimate is the hypothesis.

3. The one finiteness fact the shell needs

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_ne_top_of_eq_h10 {d : ℕ} {A : Set (HCPolySupport.Vec d)} (hA : MeasureTheory.volume A ≠ 0) {f : HCPolySupport.Vec d → ℝ} (w : HCPolySupport.H10Function A) (hf : ∀ (y : HCPolySupport.Vec d), f y = w.toFun y) : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn A) ≠ ⊤

The anchor's left-hand side is finite.

The frozen statement's u - v is, by its own two pointwise clauses, the H¹₀ witness w on x+□_n; an H¹₀ function carries its L² datum in its type, and the normalized volume measure is a finite rescaling of the restricted Lebesgue measure as soon as the window has positive volume.