Definitions

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

The bad events of ABK26, Section 3.3

This module defines local implementations of the named events of sss.bad.cubes (ABK26) as measurable subsets of the cutoff sample space, at an arbitrary triadic cube. The manuscript indexes them by an integer scale j and a centre z in 3^j Z^d; the pair (j, z) is exactly a Q : TriadicCube d with Q.scale = j and Q.index i = z_i / 3^j, and cubeSet Q = z + square_j.

The four displays

• e.Bosc.def. The oscillation event at threshold delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j} — here oscThreshold.
• e.BoscL.def. The scale-resolved oscillation event at threshold (1/5) delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j} 3^{-(L-j)/5} — here oscThresholdAt — for the single shell j_L, measured in the volume-normalized norm 3^{2j} ||grad j_L||_{W^{1,infinity}(z+square_j)}, which at p = infinity is max { 3^{2j} ||grad^2 j_L||_{L^infinity}, 3^j ||grad j_L||_{L^infinity} } (ABK26, the definition of the volume-normalized Sobolev norm; the |U|^{-1/d} factor of a cube of side 3^j is 3^{-j}).
• e.Bloc.def. The local coarse-grained ellipticity failure at q = 2, s = 1/4, threshold 10.
• e.B.def and e.Bext.def. The union, and its extension over nine generations of triadic descendants.

Reading conventions (recorded)

• badOsc is defined as the manuscript's own scale decomposition e.Bosc.decomp, i.e. as union_{L > j} B_{osc,L}(z+square_j). The manuscript's B_osc is contained in this set by e.Bosc.decomp, so badOsc is the larger event: its probability bound is the manuscript's union bound verbatim, and its complement gives at least the oscillation control the manuscript's complement gives. The reason for the choice is that the literal B_osc needs the sup norm of the derivative of the stream increment k_L - k_j, which requires a finite-sum carrier on ShellField that this repository does not have; oscGaugeSum_le_oscThreshold below proves the deterministic content of e.Bosc.decomp that does not need it.
• The L^infinity gauges localCubeDerivNorm / localCubeSecondDerivNorm are taken over the open cube, matching the proved Section 3 stream convention.

Main definitions

• cubeBasePoint: the corner-free base point z of a triadic cube.
• oscThreshold, oscThresholdAt: the two displayed thresholds.
• shellOscGauge: 3^{2j} ||grad j_L||_{W^{1,infinity}(z+square_j)}.
• badOscAt, badOsc, badLoc, bad, badExtended.

Main results

• measurable* / measurableSet_* for every gauge and event.
• oscThresholdAt_geometric_sum_le_oscThreshold: the manuscript's arithmetic (1/5) sum_{n >= 1} 3^{-n/5} <= 1 behind e.Bosc.decomp.
• oscGaugeSum_le_oscThreshold: on the complement of badOsc, the shell-wise majorant of 3^{2j} ||grad (k_L - k_j)||_{W^{1,infinity}(z+square_j)} is below the e.Bosc.def threshold, for every L >= j.

References

• ABK26, sss.bad.cubes.

The base point of a triadic cube

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.cubeBasePoint {d : ℕ} (Q : HCPolySupport.TriadicCube d) : HCPolySupport.Vec d

The manuscript's centre z in 3^j Z^d of the cube z + square_j. With this vector, cubeSet Q is the translate by cubeBasePoint Q of the centered cube of scale Q.scale.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.cubeBasePoint Q i = ↑(Q.index i) * 3 ^ Q.scale

The two oscillation thresholds

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.oscThreshold {d : ℕ} (M : ABKModel d) (j : ℤ) : ℝ

The right side of e.Bosc.def: delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j}.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.oscThreshold M j = Algsuperdiff.Section3.Provider.BadEvents.deltaOsc d * √(Algsuperdiff.Section3.Disorder.cstar M) * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑j)

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.oscThresholdAt {d : ℕ} (M : ABKModel d) (j L : ℤ) : ℝ

The right side of e.BoscL.def: (1/5) delta_osc c_star^{1/2} gamma^{-1/2} 3^{gamma j} 3^{-(L-j)/5}.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.oscThresholdAt M j L = 1 / 5 * Algsuperdiff.Section3.Provider.BadEvents.oscThreshold M j * 3 ^ (-(1 / 5) * (↑L - ↑j))

theorem Algsuperdiff.Section3.Provider.BadEvents.oscThreshold_pos {d : ℕ} (M : ABKModel d) (j : ℤ) : 0 < oscThreshold M j

The single-shell oscillation gauge

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.shellOscGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (L : ℤ) : Cutoff.CutoffSample d → ℝ

The manuscript's 3^{2j} ||grad j_L||_{W^{1,infinity}(z+square_j)} of e.BoscL.def, at the cube Q of scale j = Q.scale and shell index L.

At p = infinity the volume-normalized Sobolev norm of ABK26 is the maximum of the gradient sup norm and |U|^{-1/d} times the value sup norm; for U = z + square_j the factor |U|^{-1/d} is 3^{-j}, so the displayed quantity is max { 3^{2j} ||grad^2 j_L||_{L^infinity(U)}, 3^j ||grad j_L||_{L^infinity(U)} }.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.shellOscGauge_le_shellDerivGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (L : ℤ) (omega : Cutoff.CutoffSample d) : shellOscGauge Q L omega ≤ 3 ^ Q.scale * (Stream.localCubeDerivNorm Q.scale (Frozen.Assumptions.ShellField.translate (cubeBasePoint Q) (↑omega L)) + 3 ^ Q.scale * Stream.localCubeSecondDerivNorm Q.scale (Frozen.Assumptions.ShellField.translate (cubeBasePoint Q) (↑omega L)))

The single-shell oscillation gauge is dominated by 3^j times the proved shell derivative gauge ||grad j_L|| + 3^j ||grad^2 j_L|| on the same cube, which is the object controlled by e.nabla.jk.O.

theorem Algsuperdiff.Section3.Provider.BadEvents.measurable_shellOscGauge {d : ℕ} (Q : HCPolySupport.TriadicCube d) (L : ℤ) : Measurable (shellOscGauge Q L)

The scale-resolved oscillation event e.BoscL.def

def Algsuperdiff.Section3.Provider.BadEvents.badOscAt {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (L : ℤ) : Set (Cutoff.CutoffSample d)

B_{osc,L}(z + square_j) of e.BoscL.def (ABK26).

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_badOscAt {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) (L : ℤ) : MeasurableSet (badOscAt M Q L)

def Algsuperdiff.Section3.Provider.BadEvents.badOsc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : Set (Cutoff.CutoffSample d)

The oscillation event B_osc(z + square_j), defined as the manuscript's own scale decomposition e.Bosc.decomp (ABK26).

Equations

• Algsuperdiff.Section3.Provider.BadEvents.badOsc M Q = ⋃ (L : ℤ), ⋃ (_ : Q.scale < L), Algsuperdiff.Section3.Provider.BadEvents.badOscAt M Q L

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_badOsc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : MeasurableSet (badOsc M Q)

theorem Algsuperdiff.Section3.Provider.BadEvents.badOscAt_subset_badOsc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {L : ℤ} (hL : Q.scale < L) : badOscAt M Q L ⊆ badOsc M Q

theorem Algsuperdiff.Section3.Provider.BadEvents.shellOscGauge_le_of_notMem_badOsc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {omega : Cutoff.CutoffSample d} (homega : omega ∉ badOsc M Q) {L : ℤ} (hL : Q.scale < L) : shellOscGauge Q L omega ≤ oscThresholdAt M Q.scale L

On the complement of badOsc, every single shell above the cube scale obeys the e.BoscL.def threshold.

The local coarse-grained ellipticity event e.Bloc.def

def Algsuperdiff.Section3.Provider.BadEvents.exponentTwo : CoarseEllipticityExponent

The exponent q = 2 at which e.Bloc.def is stated.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.exponentTwo = Algsuperdiff.Section3.CoarseEllipticityExponent.finite ⟨2, Algsuperdiff.Section3.Provider.BadEvents.exponentTwo._proof_1⟩

def Algsuperdiff.Section3.Provider.BadEvents.badLoc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : Set (Cutoff.CutoffSample d)

B_loc(z + square_j) of e.Bloc.def (ABK26): the union of { lambda^{-1}_{1/4,2}(z+square_j; a_j) > 10 sigma_j^{-1} } and { Lambda_{1/4,2}(z+square_j; a_j) > 10 sigma_j }.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_badLoc {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : MeasurableSet (badLoc M Q)

The combined and extended bad events

def Algsuperdiff.Section3.Provider.BadEvents.bad {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : Set (Cutoff.CutoffSample d)

B(z + square_j) of e.B.def (ABK26).

Equations

• Algsuperdiff.Section3.Provider.BadEvents.bad M Q = Algsuperdiff.Section3.Provider.BadEvents.badOsc M Q ∪ Algsuperdiff.Section3.Provider.BadEvents.badLoc M Q

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_bad {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : MeasurableSet (bad M Q)

def Algsuperdiff.Section3.Provider.BadEvents.badExtended {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : Set (Cutoff.CutoffSample d)

The literal nine-generation extension B^*(z + square_j) of e.Bext.def (ABK26): the union of B(z' + square_{j-i}) over i in {0, ..., 9} and all triadic descendants z' + square_{j-i} of z + square_j at depth i.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.badExtended M Q = ⋃ i ∈ Finset.range 10, ⋃ R ∈ HCPolySupport.descendantsAtScale Q (Q.scale - ↑i), Algsuperdiff.Section3.Provider.BadEvents.bad M R

theorem Algsuperdiff.Section3.Provider.BadEvents.measurableSet_badExtended {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : MeasurableSet (badExtended M Q)

theorem Algsuperdiff.Section3.Provider.BadEvents.bad_subset_badExtended {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) : bad M Q ⊆ badExtended M Q

The arithmetic behind e.Bosc.decomp

theorem Algsuperdiff.Section3.Provider.BadEvents.oscThresholdAt_geometric_sum_le_oscThreshold {d : ℕ} (M : ABKModel d) (j : ℤ) (N : ℕ) : ∑ n ∈ Finset.range N, oscThresholdAt M j (j + 1 + ↑n) ≤ oscThreshold M j

The manuscript's arithmetic (1/5) sum_{n = 1}^{N} 3^{-n/5} <= 1 (ABK26, e.Bosc.decomp), in the form of the scale-resolved thresholds: the sum of the e.BoscL.def thresholds over any finite initial block of scales above j is below the e.Bosc.def threshold.

theorem Algsuperdiff.Section3.Provider.BadEvents.oscGaugeSum_le_oscThreshold {d : ℕ} (M : ABKModel d) (Q : HCPolySupport.TriadicCube d) {omega : Cutoff.CutoffSample d} (homega : omega ∉ badOsc M Q) (N : ℕ) : ∑ n ∈ Finset.range N, shellOscGauge Q (Q.scale + 1 + ↑n) omega ≤ oscThreshold M Q.scale

The deterministic content of e.Bosc.decomp available without a finite-sum carrier on ShellField: on the complement of badOsc, the shell-wise majorant of 3^{2j} ||grad (k_{j+N} - k_j)||_{W^{1,infinity}(z+square_j)} stays below the e.Bosc.def threshold, for every finite block of scales above j.