OAI/Probability/SLE/Gauge/MomentBatches.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The dyadic moment batches in Lemma gauge:multiplicity of the first paper.

  1. def OAI.SLEExactGauge.MomentBatches.dyadic line 13
  2. def OAI.SLEExactGauge.MomentBatches.weight line 15
  3. def OAI.SLEExactGauge.MomentBatches.copies line 17
  4. lemma OAI.SLEExactGauge.MomentBatches.dyadic_pos line 20
  5. lemma OAI.SLEExactGauge.MomentBatches.dyadic_step line 22
  6. lemma OAI.SLEExactGauge.MomentBatches.denominator_pos line 25
  7. lemma OAI.SLEExactGauge.MomentBatches.dyadic_sum_le line 30

    Source documentation

    A finite selection of dyadic levels below x is bounded by the complete geometric tail. Missing levels only improve the bound.

    Distinct definitions of this name: OAI/Probability/SLEGauge/MomentBatches.lean:236 (different declaration text). Qualify references as OAI.SLEExactGauge.MomentBatches.dyadic_sum_le@path.

    lemma dyadic_sum_le {n : ℕ} (hn : 1 ≤ n) (S : Finset ℤ)
    {x : ℝ} (hx : 0 ≤ x) (hS : ∀ k ∈ S, dyadic k ≤ x) :
    ∑ k ∈ S, dyadic k ^ n ≤ x ^ n / (1 - (1 / 2 : ℝ) ^ n) := by
…

    Mentions: OAI.SLEExactGauge.MomentBatches.dyadic

  8. lemma OAI.SLEExactGauge.MomentBatches.weight_nonneg line 60
  9. lemma OAI.SLEExactGauge.MomentBatches.copies_le_weight line 64
  10. lemma OAI.SLEExactGauge.MomentBatches.hit_count_upper line 71
  11. lemma OAI.SLEExactGauge.MomentBatches.integral_hit_count line 94
  12. theorem OAI.SLEExactGauge.MomentBatches.upper_batch_probability line 113

    Source documentation

    The upper batch probability estimate with its precise geometric constant. Only the positive finite nth moment of the nonnegative random mass is used.

    theorem upper_batch_probability {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P] (X : Ω → ℝ) (hX : Measurable X)
    (hX0 : ∀ ω, 0 ≤ X ω) {n : ℕ} (hn : 1 ≤ n)
    {m T : ℝ} (hm : 0 < m) (hInt : Integrable (fun ω => X ω ^ n) P)
    (hMoment : ∫ ω, X ω ^ n ∂P = m) :
    ∑' k : ℤ, (copies n m T k : ℝ) * P.real {ω | 16 * dyadic k ≤ X ω} ≤
      (4 : ℝ) ^ n / 16 ^ n / (1 - (1 / 2 : ℝ) ^ n) := by
…

    Mentions: OAI.SLEExactGauge.MomentBatches.copies, OAI.SLEExactGauge.MomentBatches.dyadic

  13. lemma OAI.SLEExactGauge.MomentBatches.floor_half_sub_half line 136
  14. lemma OAI.SLEExactGauge.MomentBatches.dyadic_level line 141
  15. lemma OAI.SLEExactGauge.MomentBatches.hit_count_lower line 152

    Source documentation

    One well-chosen dyadic level already gives the required lower count. This avoids charging a floor error at every dyadic level.

    lemma hit_count_lower {n : ℕ} (hn : 1 ≤ n) {m T x : ℝ} (hm : 0 < m)
    (hx : 0 ≤ x) (hxT : x ≤ T) (S : Finset ℤ)
    (hS : ∀ k, copies n m T k ≠ 0 → k ∈ S) :
    (2 : ℝ) ^ n / (2 * m) * x ^ n - 1 / 2 ≤
      ∑ k ∈ S, if dyadic k ≤ x then (copies n m T k : ℝ) else 0 := by
…

    Mentions: OAI.SLEExactGauge.MomentBatches.copies, OAI.SLEExactGauge.MomentBatches.dyadic

  16. theorem OAI.SLEExactGauge.MomentBatches.retained_truncated_moment line 193

    Source documentation

    The (n+1)st moment bounds the loss above the paper's cutoff T = 4 M / m; a retained 3m/4 moment leaves at least m/2.

    theorem retained_truncated_moment {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) (Y : Ω → ℝ) (hY : Measurable Y) (hY0 : ∀ ω, 0 ≤ Y ω)
    (n : ℕ) {m M : ℝ} (hm : 0 < m) (hM : 0 < M)
    (hi : Integrable (fun ω => Y ω ^ n) P)
    (hi' : Integrable (fun ω => Y ω ^ (n + 1)) P)
    (hretained : 3 * m / 4 ≤ ∫ ω, Y ω ^ n ∂P)
    (hnext : (∫ ω, Y ω ^ (n + 1) ∂P) ≤ M) :
    m / 2 ≤ ∫ ω in {ω | Y ω ≤ 4 * M / m}, Y ω ^ n ∂P := by
…
  17. theorem OAI.SLEExactGauge.MomentBatches.lower_batch_probability_finset line 231

    Source documentation

    The lower batch probability estimate. The 1/2 loss is slightly stronger than the paper's 1 / (2 * (1 - 2⁻ⁿ)) loss.

    theorem lower_batch_probability_finset {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : Ω → ℝ) (hY : Measurable Y)
    (hY0 : ∀ ω, 0 ≤ Y ω) {n : ℕ} (hn : 1 ≤ n) {m T : ℝ} (hm : 0 < m)
    (hi : Integrable (fun ω => Y ω ^ n) P)
    (htrunc : m / 2 ≤ ∫ ω in {ω | Y ω ≤ T}, Y ω ^ n ∂P)
    (S : Finset ℤ) (hS : ∀ k, copies n m T k ≠ 0 → k ∈ S) :
    (2 : ℝ) ^ n / 4 - 1 / 2 ≤
      ∑ k ∈ S, (copies n m T k : ℝ) * P.real {ω | dyadic k ≤ Y ω} := by
…

    Mentions: OAI.SLEExactGauge.MomentBatches.copies, OAI.SLEExactGauge.MomentBatches.dyadic

  18. lemma OAI.SLEExactGauge.MomentBatches.lower_constant line 273
  19. lemma OAI.SLEExactGauge.MomentBatches.copies_positive_bounds line 281
  20. lemma OAI.SLEExactGauge.MomentBatches.copies_support_finite line 303
  21. theorem OAI.SLEExactGauge.MomentBatches.lower_batch_probability line 322

    Source documentation

    The lower batch inequality for the whole integer sum, with no auxiliary finite support assumption.

    theorem lower_batch_probability {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : Ω → ℝ) (hY : Measurable Y)
    (hY0 : ∀ ω, 0 ≤ Y ω) {n : ℕ} (hn : 3 ≤ n) {m M : ℝ}
    (hm : 0 < m) (hM : 0 < M)
    (hi : Integrable (fun ω => Y ω ^ n) P)
    (hi' : Integrable (fun ω => Y ω ^ (n + 1)) P)
    (hretained : 3 * m / 4 ≤ ∫ ω, Y ω ^ n ∂P)
    (hnext : (∫ ω, Y ω ^ (n + 1) ∂P) ≤ M) :
    (2 : ℝ) ^ n / 8 ≤ ∑' k : ℤ,
      (copies n m (4 * M / m) k : ℝ) * P.real {ω | dyadic k ≤ Y ω} := by
…

    Mentions: OAI.SLEExactGauge.MomentBatches.copies, OAI.SLEExactGauge.MomentBatches.dyadic

  22. lemma OAI.SLEExactGauge.MomentBatches.copies_eq_target line 347
  23. theorem OAI.SLEExactGauge.MomentBatches.target_upper_batch_probability line 352

    Source documentation

    The upper inequality in the exact notation of the moment-gauge construction.

    theorem target_upper_batch_probability {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P] (X : Ω → ℝ) (hX : Measurable X)
    (hX0 : ∀ ω, 0 ≤ X ω) (κ : ℝ) (W : SLEExactGauge.Target.WienerLaw)
    {n : ℕ} (hn : 1 ≤ n) (hm : 0 < SLEExactGauge.Target.moment κ W n)
    (hi : Integrable (fun ω => X ω ^ n) P)
    (he : ∫ ω, X ω ^ n ∂P = SLEExactGauge.Target.moment κ W n) :
    ∑' k : ℤ, (SLEExactGauge.Target.multiplicity κ W n k : ℝ) *
      P.real {ω | 16 * (2 : ℝ) ^ k ≤ X ω} ≤
        (4 : ℝ) ^ n / 16 ^ n / (1 - (1 / 2 : ℝ) ^ n) :=
…

    Mentions: OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.moment, OAI.SLEExactGauge.Target.multiplicity

  24. theorem OAI.SLEExactGauge.MomentBatches.target_lower_batch_probability line 364

    Source documentation

    The success inequality in the exact notation of the moment-gauge construction.

    theorem target_lower_batch_probability {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : Ω → ℝ) (hY : Measurable Y)
    (hY0 : ∀ ω, 0 ≤ Y ω) (κ : ℝ) (W : SLEExactGauge.Target.WienerLaw)
    {n : ℕ} (hn : 3 ≤ n)
    (hm : 0 < SLEExactGauge.Target.moment κ W n)
    (hM : 0 < SLEExactGauge.Target.moment κ W (n + 1))
    (hi : Integrable (fun ω => Y ω ^ n) P)
    (hi' : Integrable (fun ω => Y ω ^ (n + 1)) P)
    (hretained : 3 * SLEExactGauge.Target.moment κ W n / 4 ≤ ∫ ω, Y ω ^ n ∂P)
    (hnext : (∫ ω, Y ω ^ (n + 1) ∂P) ≤ SLEExactGauge.Target.moment κ W (n + 1)) :
    (2 : ℝ) ^ n / 8 ≤ ∑' k : ℤ, (SLEExactGauge.Target.multiplicity κ W n k : ℝ) *
      P.real {ω | (2 : ℝ) ^ k ≤ Y ω} :=
…

    Mentions: OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.moment, OAI.SLEExactGauge.Target.multiplicity

  25. lemma OAI.SLEExactGauge.MomentBatches.cleanup_count_le line 378
  26. theorem OAI.SLEExactGauge.MomentBatches.cleanup_tail_bound line 399

    Source documentation

    The cleanup entries have summable tail probabilities, bounded by the first moment divided by 16. Indices n + 1 are the paper's positive integers.

    theorem cleanup_tail_bound {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P] (X : Ω → ℝ) (hX : Measurable X)
    (hX0 : ∀ ω, 0 ≤ X ω) (hi : Integrable X P) :
    Summable (fun n : ℕ => P.real {ω | 16 * ((n : ℝ) + 1) ≤ X ω}) ∧
      (∑' n : ℕ, P.real {ω | 16 * ((n : ℝ) + 1) ≤ X ω}) ≤ (∫ ω, X ω ∂P) / 16 := by
…
  27. lemma OAI.SLEExactGauge.MomentBatches.upper_constant_le_geometric line 426
  28. theorem OAI.SLEExactGauge.MomentBatches.all_batch_tails_summable line 444

    Source documentation

    Both types of entries in all positive-order batches have summable exceedance probabilities. The hypotheses are precisely the positive finite moments of one nonnegative mass, not any SLE conclusion.

    theorem all_batch_tails_summable {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P] (X : Ω → ℝ) (hX : Measurable X)
    (hX0 : ∀ ω, 0 ≤ X ω) (m T : ℕ → ℝ)
    (hm : ∀ n, 1 ≤ n → 0 < m n)
    (hi : ∀ n, 1 ≤ n → Integrable (fun ω => X ω ^ n) P)
    (hMoment : ∀ n, 1 ≤ n → (∫ ω, X ω ^ n ∂P) = m n) :
    Summable (fun n : ℕ =>
      (∑' k : ℤ, (copies (n + 1) (m (n + 1)) (T (n + 1)) k : ℝ) *
        P.real {ω | 16 * dyadic k ≤ X ω}) +
      P.real {ω | 16 * ((n : ℝ) + 1) ≤ X ω}) := by
…

    Mentions: OAI.SLEExactGauge.MomentBatches.copies, OAI.SLEExactGauge.MomentBatches.dyadic