OAI/Analysis/FiniteFactor/Sampling/MixedCorrelation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sampling_kernel_mean line 11

   Source documentation

   A bounded nonnegative coordinate kernel has a measurable bounded mean.

   theorem sampling_kernel_mean {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (u : ℝ → Ω → ℝ)
       (hu : Measurable (fun p : ℝ × Ω => u p.1 p.2)) (C : ℝ)
       (hb : ∀ s t, 0 ≤ u s t ∧ u s t ≤ C) :
       Measurable (fun s => ∫ t, u s t ∂μ) ∧
       ∀ s, 0 ≤ (∫ t, u s t ∂μ) ∧ (∫ t, u s t ∂μ) ≤ C := by
   …

2. theorem OAI.FiniteFactor.sampling_integrated_mixed_error line 27

   Source documentation

   The mixed coordinate factor inherits a relative one-phase error. The ideal moment may vanish; no division by it occurs.

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

   Mentions: OAI.FiniteFactor.unitIntervalMeasure