ClauseTwo #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The In particular bridge: clause (ii) of the annular decomposition #
The Section 4.1 proposition ends with an In particular clause that the
manuscript never derives: on the good event 𝒢(m; s, ε) and under a smallness
condition on γ|log γ|², the unsquared flux-corrected error is at most Cε.
𝒢₂bounds the first right-hand term of (i) byCε²,𝒢₁'s two conditions bound the third and fourth byC s^{−2} c⋆^{−1} γ · (s ε c⋆^{1/2} γ^{−1/2})² = Cε², and the smallness condition handles the second.
The four term budgets #
ofReal_mul_clauseOneTermOne_le_of_eventG2—𝒢₂'s bracket carries the weight3^{−(s/4)(m−n)}, the display carries3^{−s(m−n)}, so the display term is below the event's own sum ands · (term one) ≤ ε²with no loss.- With the printed
ℓ²third term this step would still work, but clause (i) itself would not; see the graph's[G-7]note. clauseOneTermFour_le_of_eventG1— the display weight3^{−(s/2)(m−n)}is below𝒢₁'s3^{−(s/4)(m−n)}slot by slot.- The printed hypothesis
γ|log γ|² ≤ s c⋆² εgives onlys² c⋆⁴ ε²and does not suffice.
Wrinkle (b): the silent square root #
Clause (i) bounds the squared supremum over L ≥ m; clause (ii) is unsquared.
indicator_observableSup_le_of_sqSup takes the square root sample by sample:
a bound B on ⨆_L ofReal(𝓔_L²) gives the bound √B on ⨆_L ofReal(𝓔_L),
because each representative is nonnegative. Since the total budget is
4 C ε², the clause-(ii) constant is 2√C.
The event #
Clause (ii) is stated on Frozen.Section4.goodEventAt M Ccg m 0 s ε, which is
by definition Cutoff.translateCutoffSample 0 ⁻¹' Support.goodEventBase …;
goodEventBase_eq_translateZero_preimage records that this is
Support.goodEventBase M Ccg m s ε itself, so the event carried below is the
frozen one at y = 0. (The frozen module is never imported.)
Part A -- the clause-(i) right-hand side as a named object #
The four-term right-hand side of the clause-(i) representative display, at
the output constant C. This is definitionally the right-hand side of
DisplaySlots.clauseOne_representative_display_latticeMax; it is a naming
convenience inside this provider module and closes no node.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The display is monotone in its output constant.
Part B -- the three event budgets #
The first term, from 𝒢₂. The display weight 3^{−s(m−n)} sits below
the event weight 3^{−(s/4)(m−n)} on the annular region n ≤ j − 1 ≤ m − 1, so
s · (term one) is bounded by the event's own threshold ε².
The fourth term, from 𝒢₁'s second condition. The display weight
3^{−(s/2)(m−n)} sits below the event weight 3^{−(s/4)(m−n)} slot by slot;
the inner k-blocks are literally the same.
Part C -- the total budget on the good event #
The clause-(i) right-hand side on the good event is at most 4 C ε².
The printed hypothesis γ|log γ|² ≤ s c⋆² ε would give only γ²|log γ|⁴ ≤ s² c⋆⁴ ε², one power of s short of the corrected s^{−3}.
Part D -- wrinkle (b): the silent square root #
Wrinkle (b), made honest. A bound on the indicator of the squared supremum gives the square root bound on the indicator of the plain supremum, sample by sample, because each flux-corrected representative is nonnegative.
Part E -- the In particular bridge #
The frozen clause-(ii) event goodEventAt M Ccg m 0 s ε unfolds to
Support.goodEventBase M Ccg m s ε: translating by 0 is the identity. The
frozen module is not imported; this records the identification at the level of
its definitional body.