OAI/MeasureTheory/Falconer/Estimates/IidSampling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Falconer.iidLaw line 19
2. instance OAI.Falconer.(instance at line 23) line 23
3. def OAI.Falconer.iidCount line 28
4. theorem OAI.Falconer.measurable_iidCount line 31
5. theorem OAI.Falconer.iid_cell_mass line 37
6. theorem OAI.Falconer.iid_indicators_independent line 50
7. theorem OAI.Falconer.iid_finite_cells_tail line 67

   Source documentation

   Counts are simultaneously controlled on every prescribed measurable cell, with an exponentially small failure probability.

   theorem iid_finite_cells_tail {X κ : Type*} [MeasurableSpace X] [DecidableEq κ]
       (ν : ProbabilityMeasure X) (n : ℕ) (B : Finset κ) (A : κ → Set X)
       (hA : ∀ j, MeasurableSet (A j)) (p T : κ → ℝ) (L : ℝ)
       (hp : ∀ j ∈ B, 0 ≤ p j)
       (hprob : ∀ j ∈ B, (ν : Measure X).real (A j) ≤ p j)
       (hT : ∀ j ∈ B, (n : ℝ) * (exp 1 - 1) * p j + L ≤ T j) :
       iidLaw ν n (⋃ j ∈ B, {ω | T j ≤ iidCount (A j) ω}) ≤
         ENNReal.ofReal ((B.card : ℝ) * exp (-L)) := by
   …

   Mentions: OAI.Falconer.iidLaw, OAI.Falconer.iidCount

8. def OAI.Falconer.iidAverage line 91
9. theorem OAI.Falconer.integrable_iidAverage line 94
10. theorem OAI.Falconer.integral_iidAverage line 102
11. theorem OAI.Falconer.iidAverage_le_one line 116
12. theorem OAI.Falconer.exists_iid_sample_with_counts_and_incidence line 127

    Source documentation

    Simultaneous cell bounds and at least half the expected incidence can be achieved by one sample of the original labels.

    theorem exists_iid_sample_with_counts_and_incidence {X κ : Type*}
        [MeasurableSpace X] [DecidableEq κ] (ν : ProbabilityMeasure X)
        {n : ℕ} (hn : 0 < n) (B : Finset κ) (A : κ → Set X)
        (hA : ∀ j, MeasurableSet (A j)) (p T : κ → ℝ) (L : ℝ)
        (hp : ∀ j ∈ B, 0 ≤ p j)
        (hprob : ∀ j ∈ B, (ν : Measure X).real (A j) ≤ p j)
        (hT : ∀ j ∈ B, (n : ℝ) * (exp 1 - 1) * p j + L ≤ T j)
        (f : X → ℝ) (hf : Integrable f (ν : Measure X)) (hf1 : ∀ x, f x ≤ 1)
        {I : ℝ} (hI : 0 < I) (hmean : I ≤ ∫ x, f x ∂(ν : Measure X))
        (hsmall : (B.card : ℝ) * exp (-L) ≤ I / 4) :
        ∃ ω : Fin n → X,
          (∀ j ∈ B, iidCount (A j) ω < T j) ∧ I / 2 ≤ iidAverage f ω := by
    …

    Mentions: OAI.Falconer.iidCount, OAI.Falconer.iidAverage

13. theorem OAI.Falconer.exists_iid_sample_scale_counts line 161

    Source documentation

    For cell masses at most K * s, only the additive term L in the sampling constant is needed to pay for simultaneous control, provided the expected scale count n * s is at least one.

    theorem exists_iid_sample_scale_counts {X κ : Type*}
        [MeasurableSpace X] [DecidableEq κ] (ν : ProbabilityMeasure X)
        {n : ℕ} (hn : 0 < n) (B : Finset κ) (A : κ → Set X)
        (hA : ∀ j, MeasurableSet (A j)) (s : κ → ℝ) {K L : ℝ}
        (hK : 0 ≤ K) (hL : 0 ≤ L)
        (hscale : ∀ j ∈ B, 1 ≤ (n : ℝ) * s j)
        (hprob : ∀ j ∈ B, (ν : Measure X).real (A j) ≤ K * s j)
        (f : X → ℝ) (hf : Integrable f (ν : Measure X)) (hf1 : ∀ x, f x ≤ 1)
        {I : ℝ} (hI : 0 < I) (hmean : I ≤ ∫ x, f x ∂(ν : Measure X))
        (hsmall : (B.card : ℝ) * exp (-L) ≤ I / 4) :
        ∃ ω : Fin n → X,
          (∀ j ∈ B, iidCount (A j) ω < ((exp 1 - 1) * K + L) * (n : ℝ) * s j) ∧
    …

    Mentions: OAI.Falconer.iidCount