OAI/MeasureTheory/Falconer/Estimates/SamplingTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Falconer.exp_indicator_one line 18
2. theorem OAI.Falconer.indicator_mgf_one line 25

   Source documentation

   The exponential moment of a Bernoulli indicator at parameter one.

   theorem indicator_mgf_one {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (A : Set Ω) (hA : MeasurableSet A) :
       mgf (A.indicator (fun _ => (1 : ℝ))) μ 1 = 1 + (exp 1 - 1) * μ.real A := by
   …

3. theorem OAI.Falconer.independent_indicator_sum_tail line 37

   Source documentation

   The tail bound retains the actual small mean of each indicator.

   theorem independent_indicator_sum_tail {Ω ι : Type*} [MeasurableSpace Ω]
       [DecidableEq ι] (μ : Measure Ω) [IsProbabilityMeasure μ]
       (A : ι → Set Ω) (hA : ∀ i, MeasurableSet (A i))
       (hindep : iIndepFun (fun i => (A i).indicator (fun _ => (1 : ℝ))) μ)
       (S : Finset ι) {p T : ℝ} (_hp : 0 ≤ p) (hprob : ∀ i ∈ S, μ.real (A i) ≤ p) :
       μ.real {ω | T ≤ ∑ i ∈ S, (A i).indicator (fun _ => (1 : ℝ)) ω} ≤
         exp ((S.card : ℝ) * (exp 1 - 1) * p - T) := by
   …

4. theorem OAI.Falconer.independent_indicator_sum_tail_le line 88

   Source documentation

   A threshold exceeding the exponential-moment mean by L fails with probability at most exp (-L).

   theorem independent_indicator_sum_tail_le {Ω ι : Type*} [MeasurableSpace Ω]
       [DecidableEq ι] (μ : Measure Ω) [IsProbabilityMeasure μ]
       (A : ι → Set Ω) (hA : ∀ i, MeasurableSet (A i))
       (hindep : iIndepFun (fun i => (A i).indicator (fun _ => (1 : ℝ))) μ)
       (S : Finset ι) {p T L : ℝ} (hp : 0 ≤ p) (hprob : ∀ i ∈ S, μ.real (A i) ≤ p)
       (hT : (S.card : ℝ) * (exp 1 - 1) * p + L ≤ T) :
       μ {ω | T ≤ ∑ i ∈ S, (A i).indicator (fun _ => (1 : ℝ)) ω} ≤
         ENNReal.ofReal (exp (-L)) := by
   …

5. theorem OAI.Falconer.finite_sample_count_failure line 103

   Source documentation

   Simultaneous sample-count bounds over any fixed finite collection of cells. Independence is required only among the draws for each cell.

   theorem finite_sample_count_failure {Ω ι κ : Type*} [MeasurableSpace Ω]
       [DecidableEq ι] [DecidableEq κ] (μ : Measure Ω) [IsProbabilityMeasure μ]
       (B : Finset κ) (S : Finset ι) (A : κ → ι → Set Ω)
       (hA : ∀ j i, MeasurableSet (A j i))
       (hindep : ∀ j ∈ B,
         iIndepFun (fun i => (A j i).indicator (fun _ => (1 : ℝ))) μ)
       (p T : κ → ℝ) (L : ℝ) (hp : ∀ j ∈ B, 0 ≤ p j)
       (hprob : ∀ j ∈ B, ∀ i ∈ S, μ.real (A j i) ≤ p j)
       (hT : ∀ j ∈ B, (S.card : ℝ) * (exp 1 - 1) * p j + L ≤ T j) :
       μ (⋃ j ∈ B, {ω | T j ≤ ∑ i ∈ S, (A j i).indicator (fun _ => (1 : ℝ)) ω}) ≤
         ENNReal.ofReal ((B.card : ℝ) * exp (-L)) := by
   …

6. theorem OAI.Falconer.exists_good_sample_incidence line 128

   Source documentation

   A small exceptional family of samples cannot carry all the expected incidence. This is the probabilistic-method selection used after the simultaneous count bound.

   theorem exists_good_sample_incidence {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (J : Ω → ℝ) (hJ : Integrable J μ)
       (hJone : ∀ ω, J ω ≤ 1) (B : Set Ω) (hB : MeasurableSet B)
       {I : ℝ} (hI : 0 < I) (hmean : I ≤ ∫ ω, J ω ∂μ)
       (hbad : μ.real B ≤ I / 4) :
       ∃ ω ∉ B, I / 2 ≤ J ω := by
   …