OneStepGoodScales

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

The good-event cap and the transport of the harmonic-approximation conclusion

Two more ingredients of l.excess.decay.good.scales, both proved outright:

• the good-event cap: ae_errorRepresentative_le_goodEventDeltaSlot is the printed 𝓔_{s/8,∞,2}(z+□_j; a_L − (κ_L−κ_j)_{z+□_j}, σ_j) · 1_𝒢 ≤ C s δ^{1/2} at the smallness parameter ε = (s/8) δ^{1/2}, obtained from the proved generic-ε annular cap. This is the leg that produces the s^{-1/2}δ^{1/2} summand of the printed contraction factor.
• the carrier transport of the harmonic-approximation anchor's left-hand side: the anchor bounds ‖u−v‖ in ℝ≥0∞ on the full moved cube y + □_{n-2}, while the triangle assembly reads ‖u−v‖_{L²(U_2)} in ℝ. normalizedL2On_truncatedWindow_le_movedReplacementCube and normalizedL2On_le_toReal_of_eLpNorm_le do the two halves, and le_of_indicator_goodEventAt_le removes the indicator after the ε-monotonicity of the good event.

The ε-monotonicity bridge

The harmonic lemma carries the indicator at one ε slot while the excess-decay display carries it at ε = (s/8)δ^{1/2}, and the source never states the inclusion between the two events. It is proved here (GoodEvents.goodEventAt_mono_ep: the event grows with ε), and le_of_indicator_goodEventAt_le is its consumption: a bound valid on the larger event 𝒢(·; s/8, 1/2) is valid pathwise on the smaller event 𝒢(·; s/8, (s/8)δ^{1/2}), which is the event the cap is available on. The side condition (s/8)δ^{1/2} ≤ 1/2 is discharged from s ≤ 1, δ ≤ 1.

Two deviations from the printed statement, both inherited

1. The s-range. The printed lemma assumes s ∈ [8γ, 1/2]. The cap here assumes s ∈ [64γ, 1] — the range at which the proved annular cap's slot s/8 lies in its own [8γ, 1/4]. The printed range fails on [8γ, 64γ) (s/8 ≥ 8γ is false there); the floor 64γ is what replaces it, and it is also the floor the frozen harmonic anchor carries.
2. The γ-smallness hypothesis. p.mathcalE.annular.decomp additionally requires γ|log γ|² ≤ (s/8)^{3/2} c⋆² ε, which l.excess.decay.good.scales does not list among its hypotheses. It is carried here as an explicit hypothesis at the instance ε = (s/8)δ^{1/2}; note it is stronger than the ε = 1/2 instance the harmonic anchor carries, by the factor (s/4)δ^{1/2}.

1. The moved replacement cube

def Algsuperdiff.Section4.Provider.ExcessDecay.movedReplacementCube {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) : Set (HCPolySupport.Vec d)

The harmonic replacement's domain at the development's window choice: the full cube y + □_{n-2} with y = wellPlacedCentre x m (n-2) (see OneStepWindows.image_add_wellPlacedCentre_subset_windowChoice).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_toReal_movedReplacementCube {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) : (MeasureTheory.volume (movedReplacementCube x m n)).toReal = (3 ^ (n - 2)) ^ d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_movedReplacementCube_ne_top {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) : MeasureTheory.volume (movedReplacementCube x m n) ≠ ⊤

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volume_movedReplacementCube_pos {d : ℕ} (x : HCPolySupport.Vec d) (m n : ℤ) : 0 < MeasureTheory.volume (movedReplacementCube x m n)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_truncatedWindow_le_movedReplacementCube {d : ℕ} {m n : ℤ} {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 2 ≤ m) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (movedReplacementCube x m n))) : Support.normalizedL2On (truncatedWindow x m (n - 2)) f ≤ √((3 ^ 2) ^ d) * Support.normalizedL2On (movedReplacementCube x m n) f

The window transfer. The anchor's L² norm lives on the full moved cube; the assembly reads it on U_2 = (x+□_{n-2}) ∩ □_m ⊆ y+□_{n-2}. The cost is the volume ratio 3^{2d} (the truncated window's own aspect ratio).

2. The ℝ≥0∞ → ℝ bridge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_le_toReal_of_eLpNorm_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hW0 : 0 < MeasureTheory.volume W) (hWtop : MeasureTheory.volume W ≠ ⊤) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) {B : ENNReal} (hB : B ≠ ⊤) (h : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn W) ≤ B) : Support.normalizedL2On W f ≤ B.toReal

The anchor's left-hand side is an eLpNorm against the normalized volume measure; normalizedL2On is its toReal.

3. The ε-monotonicity bridge

theorem Algsuperdiff.Section4.Provider.ExcessDecay.le_of_indicator_goodEventAt_le {d : ℕ} {M : Section3.ABKModel d} {Ccg : ℝ} {j : ℤ} {z : HCPolySupport.Vec d} {t : { t : ℝ // 0 < t }} {ep : ℝ} (hep0 : 0 ≤ ep) (heple : ep ≤ 1 / 2) {F : Section3.Cutoff.CutoffSample d → ENNReal} {B : ENNReal} {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Frozen.Section4.goodEventAt M Ccg j z t ep) (h : (Frozen.Section4.goodEventAt M Ccg j z t (1 / 2)).indicator F omega ≤ B) : F omega ≤ B

Removing the anchor's indicator on the smaller event.

The good event grows with ε, so a bound stated with the indicator of 𝒢(j,z; t, 1/2) holds pathwise at every ω of 𝒢(j,z; t, ε) for ε ≤ 1/2 --- in particular at ε = (s/8)δ^{1/2}, the slot the excess-decay display and the good-event cap are written at.

4. The good-event cap at the δ^{1/2}-graded slot

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_errorRepresentative_le_goodEventDeltaSlot (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ s ∈ Set.Icc (64 * M.gamma) 1, ∀ (hs : 0 < s), ∀ delta ∈ Set.Ioc 0 1, M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (s / 8 * √delta) → ∀ (j : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) j z ⟨s / 8, ⋯⟩ (s / 8 * √delta) → ∀ (L : ℤ), j ≤ L → Support.fluxCorrectedErrorRepresentative M L j ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ C * s * √delta

The good-event cap.

  𝓔_{s/8,∞,2}(z+□_j; a_L − (κ_L−κ_j)_{z+□_j}, σ_j) · 1_{𝒢(j,z; s/8, (s/8)δ^{1/2})}
      ≤ C s δ^{1/2} .

Exactly the printed C s δ^{1/2} (the proved cap gives C·ε at ε = (s/8)δ^{1/2}, and C(s/8)δ^{1/2} ≤ C s δ^{1/2}). See deviations 1--2 of the module docstring for the two inherited hypotheses.

5. The assembly, fed by an L² bound on the moved cube

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_of_movedCubeBound {d : ℕ} (hd : d ≠ 0) {m n : ℤ} {k : ℕ} (hk : 3 ≤ k) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 1 ≤ m) {u v : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) (huv : MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => u y - v y) 2 (MeasureTheory.volume.restrict (movedReplacementCube x m n))) {Gv : HCPolySupport.Vec d → HCPolySupport.Vec d} {K Kh Csch D : ℝ} (hK : 0 ≤ K) (hCsch : 0 ≤ Csch) (hint : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (p : HCPolySupport.Vec d) => Gv p i) (truncatedWindow x m (n - 3)) MeasureTheory.volume) (hgrad : Support.HasGradientOn (truncatedWindow x m (n - 3)) v Gv) (hhol : Support.HolderSeminormBoundOn (truncatedWindow x m (n - 3)) (1 / 2) K Gv) (hschauder : K ≤ Csch * (3 ^ (-n)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m (n - 2)) v + Kh) (hD : (Support.normalizedL2On (movedReplacementCube x m n) fun (y : HCPolySupport.Vec d) => u y - v y) ≤ D) : Support.affineExcess (truncatedWindow x m (n - ↑k)) u ≤ taylorContractionConst d * Csch * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u + triangleRemainderConst d Csch k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * D)) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * Kh

The triangle assembly composed with the harmonic-approximation transport.

The ‖u-v‖ leg of excessDecay_oneStep_triangle_of_schauder is fed by any bound D on the anchor's own object --- the normalized L² norm of u - v on the full moved cube y+□_{n-2} --- paying only the transfer constant √((3^2)^d) = 3^d.