OAI/Analysis/FiniteFactor/Sampling/IntervalSums.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingClosedIndicator line 10
2. theorem OAI.FiniteFactor.samplingClosedIndicator_measurable line 13
3. theorem OAI.FiniteFactor.samplingClosedIndicator_bounds line 16
4. theorem OAI.FiniteFactor.samplingClosedIndicator_integral line 20
5. theorem OAI.FiniteFactor.samplingClosedIndicator_pair line 27
6. theorem OAI.FiniteFactor.sampling_two_intervals_pair line 43

   Source documentation

   Two intervals in each variable cost four rectangle discrepancies.

   theorem sampling_two_intervals_pair {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y) (δ : ℝ)
       (hrect : ∀ a b c d : ℝ,
         |(μ {x | X x ∈ Set.Icc a b ∧ Y x ∈ Set.Icc c d}).toReal -
           (unitIntervalMeasure (Set.Icc a b)).toReal*(unitIntervalMeasure (Set.Icc c d)).toReal| ≤ δ)
       (a b c d : Fin 2 → ℝ) :
       |(∫ x, (∑ j, samplingClosedIndicator (a j) (b j) (X x))*
           (∑ k, samplingClosedIndicator (c k) (d k) (Y x)) ∂μ) -
         (∫ t, ∑ j, samplingClosedIndicator (a j) (b j) t ∂unitIntervalMeasure)*
         (∫ t, ∑ k, samplingClosedIndicator (c k) (d k) t ∂unitIntervalMeasure)| ≤ 4*δ := by
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.samplingClosedIndicator