GoodEventCaps #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The good-event caps: 𝓔·1_𝒢 ≤ C and max{σ⁻¹Λ, σλ⁻¹}·1_𝒢 ≤ C #
This module assembles the good-event caps of ABK26 — the displays
e.good.set.giveth.v2 and e.bound.Lambdas.by.Es.v2 — from the frozen
annular anchor Algsuperdiff.Frozen.Section4.annular_decomposition (clause
(ii)) and the Λ/λ algebra of LambdaCaps.lean.
The extraction, and the term analysis it replaces #
That analysis is not redone here: the frozen theorem's clause (ii)
already packages all four groups into the single bound ≤ C ε under exactly
that hypothesis, so this module consumes the conclusion, never the proof.
Parameter plumbing (verified below, not assumed) #
The harmonic anchor's slot is (s/8, ε = 1/2) with s ∈ [64γ, 1]; the
annular anchor demands s/8 ∈ [8γ, 1/4] and ε ∈ (0, 1/2].
s ≥ 64γ ⟹ s/8 ≥ 8γ, ands ≤ 1 ⟹ s/8 ≤ 1/8 ≤ 1/4— both discharged byannularSlot_mem_Icc, so the wholes-range of the harmonic statement is admissible.ε = 1/2 ∈ (0, 1/2]— the right endpoint, discharged byhalf_mem_Ioc.- The harmonic anchor's second hoisted hypothesis is literally the annular
clause-(ii) hypothesis at this slot. That identity is machine-certified,
not asserted:
ae_boundLambdasByEs_harmonicSlotbinds the hypothesis in the harmonic statement's own syntax and discharges the generic lemma's requirement byexact, with no rewriting. Likewise the first hoisted hypothesisγ ≤ C⁻¹ c⋆¹⁰is the annular standing regime verbatim.
The constant C produced below is the annular anchor's own constant;
a consumer that must satisfy both anchors' regime hypotheses at one constant
takes a maximum, which is the standard §4 pattern.
Main results #
annularSlot_mem_Icc,half_mem_Ioc— the parameter plumbing.ae_errorObservableSup_le_of_mem_goodEventAt— clause (ii) read at the translated centrez: the[0,∞]-valuedsup_{L ≥ m}observable is≤ C εon the event𝒢(m, z; t, ε).ae_errorRepresentative_le_of_mem_goodEventAt— the caps step (e.good.set.giveth.v2's payoff): the real-valued per-L𝓔_{t,∞,2}(z+□_m; a_L − (κ_L−κ_m)_{z+□_m}, σ_m)is≤ C εon the event.ae_boundLambdasByEs—e.bound.Lambdas.by.Es.v2:max{σ_m⁻¹Λ_{t,2}, σ_mλ_{t,2}⁻¹} ≤ 2d((Cε)² + 1)on the event.ae_errorRepresentative_le_harmonicSlot,ae_boundLambdasByEs_harmonicSlot— the two headline results at the harmonic statement's own slot(s/8, ε = 1/2)and its own binders.
Deviations from print, recorded #
- The index/cube of the cap. The printed
e.bound.Lambdas.by.Es.v2is stated at the child cubex+□_{n+1}and indexs/4; the caps proved here are at the parent cubez+□_{n+2}and indexs/8, which is where the annular anchor delivers and where no index change is needed. They are NOT assumed here; no declaration below takes them as a hypothesis. Consequently the printed display's first two inequalities are out of scope for this module, and the good-event caps they carry remain open. - The comparator. See
LambdaCaps.lean: the printed display mixesσ_n⁻¹Λwithσ_{n+1}λ⁻¹whereas the cited lemma uses a singleσ₀; we follow the lemma atσ₀ = σ_m.
References #
- ABK26,
e.good.set.giveth.v2ande.bound.Lambdas.by.Es.v2. - ABK26,
e.mathcalE.annular.decomp.good.event.
1. Parameter plumbing #
The ruled ε slot is the right endpoint of the annular ε-range.
2. Clause (ii) at a translated centre #
Annular clause (ii), read at the centre z.
The frozen theorem states clause (ii) at the origin centre 0 and at the
untranslated sample. Composing with the law-preserving
Cutoff.translateCutoffSample z (proved:
GoodEvents.measurePreserving_translateCutoffSample, valid for every real z)
and using the preimage shape of the frozen goodEventAt turns it into the
statement at the centre z and the z-translated sample — the convention
resolution A4 fixes, and the one the harmonic statement's right-hand side uses.
3. The caps step #
The caps step: 𝓔 · 1_𝒢 ≤ C ε, real-valued and per-L.
This is the payoff of e.good.set.giveth.v2 that the harmonic statement's
right-hand side actually reads: the flux-corrected (∞,2) representative
𝓔_{t,∞,2}(z+□_m; a_L − (κ_L−κ_m)_{z+□_m}, σ_m) at the z-translated
sample, for every L ≥ m.
Only the third inequality of the printed display (the ≤ C) is proved
here; the first two are out of scope, see deviation 1 in the module
docstring.
4. e.bound.Lambdas.by.Es.v2 #
e.bound.Lambdas.by.Es.v2 at the annular slot.
The good-event cap on the coarse-grained ellipticity ratios of the flux-corrected field:
max{ σ_m⁻¹ Λ_{t,2}(z+□_m; a_L − (κ_L−κ_m)_{z+□_m}) ,
σ_m λ_{t,2}⁻¹(z+□_m; a_L − (κ_L−κ_m)_{z+□_m}) } · 1_𝒢 ≤ 2d((Cε)² + 1) .
The right-hand side is a constant C(d), which is what the coarse-grained
Caccioppoli step e.energy.bound.interior consumes; see deviations 1, 3, 4
in the module docstring for the three ways this differs from the printed
display.
5. The harmonic statement's own slot #
The caps step at the harmonic statement's slot (s/8, ε = 1/2).
Every hypothesis below is transcribed from
Algsuperdiff/Frozen/Section4/HarmonicApproximation.lean in that file's own
syntax; the annular window and ε-range requirements are derived, and the
smallness hypothesis is handed to the generic lemma by exact, which
machine-certifies that the harmonic anchor's second hoisted hypothesis is
literally annular clause (ii)'s hypothesis at this slot.