OAI/Analysis/FiniteFactor/Sampling/SecondDiscrepancy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_level_pair_integral line 10
2. theorem OAI.FiniteFactor.samplingTestedSecond_pair_bound line 25

   Source documentation

   The actual second-oriented reciprocal inherits rectangle discrepancy, including both monotone pieces, cutoff jumps and reflected interval tests.

   theorem samplingTestedSecond_pair_bound {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y)
       [NullSingletonClass (μ.map X)] [NullSingletonClass (μ.map Y)]
       (hXs : ∀ᵐ x ∂μ.map X, x ∈ Set.Ico (0 : ℝ) 1)
       (hYs : ∀ᵐ x ∂μ.map Y, x ∈ Set.Ico (0 : ℝ) 1)
       (δ : ℝ) (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| ≤ δ)
       (h α : ℝ) (G : Set ℝ) (a c s : ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hG : MeasurableSet G)
       (hs : s ∈ Set.Ico (0 : ℝ) 1) :
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure