OAI/Analysis/FiniteFactor/Sampling/IntegratedCorrelation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_bounded_product_integrable line 11

   Source documentation

   Bounded nonnegative products are integrable, uniformly in their parameters.

   theorem sampling_bounded_product_integrable {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsFiniteMeasure μ] (f g : Ω → ℝ) (hf : Measurable f) (hg : Measurable g)
       (C : ℝ) (hfb : ∀ x, 0 ≤ f x ∧ f x ≤ C) (hgb : ∀ x, 0 ≤ g x ∧ g x ≤ C) :
       Integrable (fun x => f x*g x) μ := by
   …

2. theorem OAI.FiniteFactor.sampling_integrated_pair_error line 23

   Source documentation

   Integrate the actual pointwise pair error over the marginal coordinate.

   theorem sampling_integrated_pair_error {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y)
       (u : ℝ → ℝ → ℝ) (hu : Measurable (fun p : ℝ × ℝ => u p.1 p.2))
       (C ε : ℝ) (hb : ∀ s t, 0 ≤ u s t ∧ u s t ≤ C)
       (he : ∀ᵐ s ∂unitIntervalMeasure,
         |(∫ x, u s (X x)*u s (Y x) ∂μ)-(∫ t, u s t ∂unitIntervalMeasure)^2| ≤ ε) :
       |(∫ s, ∫ x, u s (X x)*u s (Y x) ∂μ ∂unitIntervalMeasure)-
         (∫ s, (∫ t, u s t ∂unitIntervalMeasure)^2 ∂unitIntervalMeasure)| ≤ ε := by
   …

   Mentions: OAI.FiniteFactor.unitIntervalMeasure