CountableMaskedError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.nonnegative_series_cauchy_schwarz line 12

Source documentation

Cauchy--Schwarz for genuinely infinite nonnegative coefficient series.

theorem nonnegative_series_cauchy_schwarz {ι : Type*} (f g : ι → ℝ)
    (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
    (hfs : Summable (fun i => f i^2)) (hgs : Summable (fun i => g i^2)) :
    Summable (fun i => f i*g i) ∧
    (∑' i, f i*g i) ≤ Real.sqrt (∑' i, f i^2)*Real.sqrt (∑' i, g i^2) := by
…

theorem OAI.FiniteFactor.countable_error_integral_le line 31

Source documentation

Probability-space Cauchy--Schwarz after the pointwise series estimate. Equivalent to the product-with-counting-measure argument; no independence or finite truncation is assumed.

theorem countable_error_integral_le {Ω ι : Type*} [MeasurableSpace Ω] [Countable ι]
    {μ : Measure Ω} [IsProbabilityMeasure μ] (f g : ι → Ω → ℝ) (δ : ℝ)
    (hf : ∀ i, Measurable (f i)) (hg : ∀ i, Measurable (g i))
    (hf0 : ∀ i ω, 0 ≤ f i ω) (hg0 : ∀ i ω, 0 ≤ g i ω)
    (hfs : ∀ᵐ ω ∂μ, Summable (fun i => f i ω^2))
    (hgs : ∀ᵐ ω ∂μ, Summable (fun i => g i ω^2))
    (hfi : Integrable (fun ω => ∑' i, f i ω^2) μ)
    (hfm : (∫ ω, (∑' i, f i ω^2) ∂μ) ≤ δ)
    (hg1 : ∀ᵐ ω ∂μ, (∑' i, g i ω^2) ≤ 1) :
    Integrable (fun ω => ∑' i, f i ω*g i ω) μ ∧
    (∫ ω, (∑' i, f i ω*g i ω) ∂μ) ≤ Real.sqrt δ := by
…