Carrier

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

The sample carrier of the full stream matrix

Algsuperdiff.Section3.Cutoff.CutoffSample carries exactly the descending convergence needed by the lower-infinite cutoffs k_m = Σ_{n ≤ m} j_n. The full normalized field k(x) = Σ_{n ∈ ℤ} (j_n(x) - j_n(0)) needs the ascending half as well, and needs it quantitatively, since the size of k on a cube of scale ℓ is governed by the two tails at that scale.

This module adds the two ascending conditions to that carrier and builds the resulting sample space and its law. The carrier is the event itself: no value is assigned off it, and every statement about the field is a statement on the carrier.

Main definitions

• FullTailGood γ ω — lower-tail goodness, the sharp two-sided rates, and the ascending gradient condition on the countable family of cubes y + □_n with y rational.
• FullSample d γ — the subtype of CutoffSample d cut out by FullTailGood γ.
• fullSampleLaw M — the induced probability law.

Main results

• measurableSet_fullTailGood, ae_fullTailGood — the event is measurable and has full probability.
• map_fullSampleLaw_val — pushing the law forward recovers the cutoff-sample law, so every cutoff statement transports to the new carrier.

References

• ABK26, the stream matrix and its scale decomposition.

def Algsuperdiff.Section5.Field.ratPoint {d : ℕ} (y : Fin d → ℚ) : HCPolySupport.Vec d

The points of Vec d with rational coordinates: the countable family of cube centres on which the ascending gradient condition is imposed.

Equations

• Algsuperdiff.Section5.Field.ratPoint y i = ↑(y i)

@[simp]

theorem Algsuperdiff.Section5.Field.ratPoint_zero {d : ℕ} : ratPoint 0 = 0

def Algsuperdiff.Section5.Field.FullTailGood {d : ℕ} (gamma : ℝ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The full-tail event. Lower-tail goodness is already carried by the ambient CutoffSample; this adds the ascending half in two forms.

The sharp conjunct gives one sample constant for the two pointwise shell rates at every shell/cube crossover. For an admissible model exponent those rates imply the former quantitative two-leg growth condition.

The final conjunct is the ascending gradient condition on the countable family of cubes y + □_n with rational centres. It supplies local summability for the field at an arbitrary exponent and is also the bridge to the Section 5.1 large-scale event: it is that event on the same cubes, written with bounded partial sums instead of a threshold, and exists_mem_largeScaleEvent_of_upperGradBounded turns it into membership of Algsuperdiff.Section5.Support.largeScaleEvent at a finite threshold, the form the large-scale estimates consume. It is carried on the field's carrier so that the field and those estimates speak about one and the same sample.

Equations

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

theorem Algsuperdiff.Section5.Field.fullTailGood_sharp {d : ℕ} {gamma : ℝ} {omega : Section3.Cutoff.CutoffSample d} (h : FullTailGood gamma omega) : SharpTailGood gamma omega

theorem Algsuperdiff.Section5.Field.fullTailGood_upperGrad {d : ℕ} {gamma : ℝ} {omega : Section3.Cutoff.CutoffSample d} (h : FullTailGood gamma omega) (n : ℤ) (y : Fin d → ℚ) : UpperGradBounded n (ratPoint y) omega

def Algsuperdiff.Section5.Field.fullTailGoodSet (d : ℕ) (gamma : ℝ) : Set (Section3.Cutoff.CutoffSample d)

The measurable set cut out by the full-tail event.

Equations

• Algsuperdiff.Section5.Field.fullTailGoodSet d gamma = {omega : Algsuperdiff.Section3.Cutoff.CutoffSample d | Algsuperdiff.Section5.Field.FullTailGood gamma omega}

theorem Algsuperdiff.Section5.Field.measurableSet_fullTailGood (d : ℕ) (gamma : ℝ) : MeasurableSet (fullTailGoodSet d gamma)

theorem Algsuperdiff.Section5.Field.ae_fullTailGood {d : ℕ} (M : Section3.ABKModel d) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), FullTailGood M.gamma omega

The full-tail event has probability one.

The carrier and its law

@[reducible, inline]

abbrev Algsuperdiff.Section5.Field.FullSample (d : ℕ) (gamma : ℝ) : Type

The sample carrier of the full stream matrix: the elements of the cutoff-sample carrier on which both tails of the scale decomposition converge, the ascending one quantitatively.

Equations

• Algsuperdiff.Section5.Field.FullSample d gamma = { omega : Algsuperdiff.Section3.Cutoff.CutoffSample d // Algsuperdiff.Section5.Field.FullTailGood gamma omega }

theorem Algsuperdiff.Section5.Field.fullTailGood_growth {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : ∃ (C : ℕ), StreamGrowthBounded C ↑omega

On the carrier at the exponent of an ABK model, the sharp rates recover the original quantitative two-leg growth condition.

theorem Algsuperdiff.Section5.Field.ae_mem_range_fullSample_val {d : ℕ} (M : Section3.ABKModel d) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Set.range Subtype.val

noncomputable def Algsuperdiff.Section5.Field.fullSampleLaw {d : ℕ} (M : Section3.ABKModel d) : MeasureTheory.ProbabilityMeasure (FullSample d M.gamma)

The canonical probability law restricted to the full-tail carrier.

Equations

• Algsuperdiff.Section5.Field.fullSampleLaw M = ⟨MeasureTheory.Measure.comap Subtype.val ↑(Algsuperdiff.Section3.Cutoff.cutoffSampleLaw M), ⋯⟩

theorem Algsuperdiff.Section5.Field.map_fullSampleLaw_val {d : ℕ} (M : Section3.ABKModel d) : MeasureTheory.Measure.map Subtype.val ↑(fullSampleLaw M) = ↑(Section3.Cutoff.cutoffSampleLaw M)

Pushing the induced full-sample law forward along Subtype.val recovers the cutoff-sample law.