WaveOscillationsCore

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

The random-truncation Orlicz core of p.bfA.multiscalebound, Step 2

ABK26, proof of Proposition p.bfA.multiscalebound, Step 2, assembles the wave amplitude ||k_ell - k_{ell - hsep}|| out of a random number of layers. The manuscript writes that assembly as the random-index sum

  ||k_ell - k_{ell - hsep}||  =  sum_{h = 0}^infty  1_{{hsep = h}} ||k_ell - k_{ell-h}|| ,

each summand being an e.indc.O.sigma indicator times an increment amplitude, recombined by e.multGammasig and the countable Gamma_sigma triangle inequality.

This module supplies that assembly abstractly, in the layer-decomposed shape, over an arbitrary finite measure space and an arbitrary N-valued truncation index.

Two deliberate changes of form against the manuscript

• 1_{{i < N}} in place of 1_{{N = h}}. On a sum of nonnegative per-layer quantities the two decompositions are the same bookkeeping, sum_h 1_{{N = h}} sum_{i < h} Y_i = sum_i 1_{{i < N}} Y_i, but only the i-form has measurable summands without a measurable handle on the random index itself. Since the countable triangle inequality Provider.Orlicz.isBigOWith_gammaSigma_tsum demands measurable summands, the i-form is the only one this tree can carry.
• The Gamma_2 factor is the per-layer amplitude, not a whole increment norm. That is a property of the consumer (WaveOscillations.lean), but it is what makes the abstract statement below usable: the family Y i it takes is a family of per-layer gauges, whose Gamma_2 tails are the proved single-shell displays.

Main definitions

• Algsuperdiff.Section3.Provider.Multiscale.truncationIndicatorScale: the scale (K 3^{-b i})^{(1-sigma)/sigma_2} at which e.indc.O.sigma prices the indicator of {i < N}.

Main results

• Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_indicator_of_one_le: the trivial branch 1_E <= O_{Gamma_sigma}(A) for A >= 1.
• Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_indicator_natLt: ABK26's e.indc.O.sigma at the events {i < N}, derived from the Gamma_{1-sigma} tail of 3^{b N}.
• Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_truncatedSum: the truncated-sum assembly, e.multGammasig termwise followed by the countable Gamma_sigma triangle inequality.

References

• ABK26, proof of p.bfA.multiscalebound, Step 2.
• ABK26, e.indc.O.sigma; e.multGammasig; l.Gamma.sigma.triangle.

The trivial branch: an indicator against a scale >= 1

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_indicator_of_one_le {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {sigma A : ℝ} {E : Set Omega} (hA : 1 ≤ A) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma) (E.indicator fun (x : Omega) => 1) A

An indicator is O_{Gamma_sigma}(A) for any A >= 1: the tail event {1_E > A t} is empty for t >= 1. This covers the finitely many indices at which the quantitative e.indc.O.sigma scale of isBigOWith_gammaSigma_indicator_natLt already exceeds 1.

e.indc.O.sigma at the events {i < N}

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.truncationIndicatorScale (b sigma sigma2 K : ℝ) (i : ℕ) : ℝ

The scale at which e.indc.O.sigma prices the indicator of {i < N}, given the Gamma_{1-sigma} tail 3^{b N} <= O_{Gamma_{1-sigma}}(K):

  truncationIndicatorScale b sigma sigma_2 K i  =  (K 3^{-b i})^{(1-sigma)/sigma_2} ,

i.e. the manuscript's C 3^{-(1-sigma) b t h} at t = 1/sigma_2.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.truncationIndicatorScale b sigma sigma2 K i = (K * 3 ^ (-(b * ↑i))) ^ ((1 - sigma) / sigma2)

theorem Algsuperdiff.Section3.Provider.Multiscale.truncationIndicatorScale_pos {b sigma sigma2 K : ℝ} (hK : 0 < K) (i : ℕ) : 0 < truncationIndicatorScale b sigma sigma2 K i

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_indicator_natLt {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {N : Omega → ℕ} {b sigma sigma2 K : ℝ} (hb : 0 < b) (hsigma2 : 0 < sigma2) (hsigma : 0 < 1 - sigma) (hK : 0 < K) (htail : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (1 - sigma)) (fun (omega : Omega) => 3 ^ (b * ↑(N omega))) K) (i : ℕ) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma2) ({omega : Omega | i < N omega}.indicator fun (x : Omega) => 1) (truncationIndicatorScale b sigma sigma2 K i)

ABK26's e.indc.O.sigma at the truncation events {i < N}.

From the Gamma_{1-sigma} tail 3^{b N} <= O_{Gamma_{1-sigma}}(K) (the manuscript's e.hsep.tails),

  1_{{i < N}}  <=  O_{Gamma_{sigma_2}}( (K 3^{-b i})^{(1-sigma)/sigma_2} )     for all i in N,

which is the manuscript's O_{Gamma_{1/t}}(^{-(1-sigma) b t h}) at t = 1/sigma_2. The statement is uniform in i: for the finitely many i with 3^{b i} < K the quantitative branch is unavailable, and there the scale exceeds 1, so isBigOWith_gammaSigma_indicator_of_one_le applies.

The truncated-sum assembly

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_truncatedSum {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {N : Omega → ℕ} {Y : ℕ → Omega → ℝ} {a B : ℕ → ℝ} {sigma1 sigma2 : ℝ} (hsigma1 : 0 < sigma1) (hsigma2 : 0 < sigma2) (hNm : ∀ (i : ℕ), MeasurableSet {omega : Omega | i < N omega}) (hYm : ∀ (i : ℕ), Measurable (Y i)) (hY0 : ∀ (i : ℕ) (omega : Omega), 0 ≤ Y i omega) (ha : ∀ (i : ℕ), 0 < a i) (hB : ∀ (i : ℕ), 0 < B i) (hYO : ∀ (i : ℕ), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma1) (Y i) (a i)) (hBO : ∀ (i : ℕ), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigma2) ({omega : Omega | i < N omega}.indicator fun (x : Omega) => 1) (B i)) (hsum : Summable fun (i : ℕ) => a i * B i) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (sigma1 * sigma2 / (sigma1 + sigma2))) (fun (omega : Omega) => ∑ i ∈ Finset.range (N omega), Y i omega) (HCPolySupport.IndependentSums.gammaTriangleConst (sigma1 * sigma2 / (sigma1 + sigma2)) * ∑' (i : ℕ), HCPolySupport.Book.Ch04.gammaProductConst sigma1 sigma2 * (a i * B i))

The truncated-sum assembly of Step 2.

Given a family of nonnegative measurable per-layer variables Y i with Gamma_{sigma_1} tails at scales a i, and a truncation index N whose indicators 1_{{i < N}} carry Gamma_{sigma_2} tails at scales B i, the randomly truncated sum obeys

  sum_{i < N}  Y i  <=  O_{Gamma_tau}( Gamma_triangle(tau) * sum'_i C(sigma_1,sigma_2) a_i B_i ) ,
  tau = sigma_1 sigma_2 / (sigma_1 + sigma_2) .

This is e.multGammasig applied termwise to Y i * 1_{{i < N}}, followed by the countable Gamma_sigma triangle inequality Provider.Orlicz.isBigOWith_gammaSigma_tsum.