OAI/Analysis/FiniteFactor/Sampling/TestedFirstMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingTestedFirstWeight line 9
2. def OAI.FiniteFactor.samplingTestedFirstDensity line 13
3. theorem OAI.FiniteFactor.samplingTestedFirstWeight_measurable line 16
4. theorem OAI.FiniteFactor.samplingTestedFirstWeight_bounds line 24
5. theorem OAI.FiniteFactor.samplingWeight_integrable line 32
6. theorem OAI.FiniteFactor.samplingTestedFirstDensity_measurable line 41
7. theorem OAI.FiniteFactor.samplingTestedFirstDensity_bounds line 47

   Source documentation

   Tests decrease the exact first marginal, which is at most one.

   theorem samplingTestedFirstDensity_bounds (b : Bool) (h α : ℝ) (E G : Set ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hE : MeasurableSet E) (hG : MeasurableSet G)
       (s : ℝ) (hs : s ∈ Set.Ico (0 : ℝ) 1) :
       0 ≤ samplingTestedFirstDensity b h α E G s ∧
       samplingTestedFirstDensity b h α E G s ≤ 1 := by
   …

   Mentions: OAI.FiniteFactor.samplingTestedFirstDensity

8. theorem OAI.FiniteFactor.samplingTestedFirstDensity_square line 71

   Source documentation

   The first tested marginal has quadratic moment at most one in both triangular and diagonal coordinates, uniformly in the measurable tests.

   theorem samplingTestedFirstDensity_square (b : Bool) (h α : ℝ) (E G : Set ℝ)
       (hh : 0 < h) (hh1 : h < 1) (hα : 0 < α) (hE : MeasurableSet E) (hG : MeasurableSet G) :
       (∫ s, samplingTestedFirstDensity b h α E G s ^ 2 ∂unitIntervalMeasure) ≤ 1 := by
   …

   Mentions: OAI.FiniteFactor.samplingTestedFirstDensity, OAI.FiniteFactor.unitIntervalMeasure