TailEstimate.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.conditional_mask_integral_le line 19

Source documentation

A conditional probability bound controls any nonnegative integrable weight measurable with respect to the conditioning sigma algebra.

theorem conditional_mask_integral_le [IsFiniteMeasure μ]
    {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {f : Ω → ℝ} {H : Set Ω} {δ : ℝ}
    (hf : Integrable f μ) (hfm : StronglyMeasurable[m] f)
    (hf0 : 0 ≤ᵐ[μ] f) (hH : @MeasurableSet Ω mΩ H)
    (hcond : ∀ᵐ ω ∂μ, μ[H.indicator (fun _ => (1 : ℝ)) | m] ω ≤ δ) :
    ∫ ω in H, f ω ∂μ ≤ δ * ∫ ω, f ω ∂μ := by
…

theorem OAI.FiniteFactor.integral_mul_le_sqrt_squares line 46

Source documentation

Cauchy–Schwarz in the integral form used on Ω × ℤ.

theorem integral_mul_le_sqrt_squares {f g : Ω → ℝ}
    (hf : MemLp f 2 μ) (hg : MemLp g 2 μ)
    (hf0 : 0 ≤ᵐ[μ] f) (hg0 : 0 ≤ᵐ[μ] g) :
    ∫ ω, f ω * g ω ∂μ ≤
      Real.sqrt (∫ ω, f ω ^ 2 ∂μ) * Real.sqrt (∫ ω, g ω ^ 2 ∂μ) := by
…

theorem OAI.FiniteFactor.integral_mul_le_sqrt_of_square_bounds line 59

Source documentation

A masked L² mass at most δ and an unmasked mass at most one yield √δ. The ambient measure can be probability times counting measure, so this is not restricted to a finite coefficient set.

theorem integral_mul_le_sqrt_of_square_bounds {f g : Ω → ℝ} {δ : ℝ}
    (hf : MemLp f 2 μ) (hg : MemLp g 2 μ)
    (hf0 : 0 ≤ᵐ[μ] f) (hg0 : 0 ≤ᵐ[μ] g)
    (hδ : ∫ ω, f ω ^ 2 ∂μ ≤ δ) (hg1 : ∫ ω, g ω ^ 2 ∂μ ≤ 1) :
    ∫ ω, f ω * g ω ∂μ ≤ Real.sqrt δ := by
…

theorem OAI.FiniteFactor.conditional_mask_tsum_integral_le line 76

Source documentation

Countably many masks, each with a conditional probability bound. The sum is genuinely infinite; no bound on the union of the events is used. Apply to f_v=|ξ_v(x)|² or f_v=|γ_{n+v}(y)|² in the two orientations.

theorem conditional_mask_tsum_integral_le [IsFiniteMeasure μ]
    {ι : Type*} [Countable ι] {m : MeasurableSpace Ω} (hm : m ≤ mΩ)
    {f : ι → Ω → ℝ} {H : ι → Set Ω} {δ : ℝ}
    (hf : ∀ i, Integrable (f i) μ)
    (hfm : ∀ i, StronglyMeasurable[m] (f i))
    (hf0 : ∀ i ω, 0 ≤ f i ω) (hH : ∀ i, @MeasurableSet Ω mΩ (H i))
    (hsum : ∀ᵐ ω ∂μ, Summable (fun i => f i ω))
    (hint : Integrable (fun ω => ∑' i, f i ω) μ)
    (hcond : ∀ i, ∀ᵐ ω ∂μ,
      μ[(H i).indicator (fun _ => (1 : ℝ)) | m] ω ≤ δ) :
    ∫ ω, (∑' i, (H i).indicator (f i) ω) ∂μ ≤
      δ * ∫ ω, (∑' i, f i ω) ∂μ := by
…

theorem OAI.FiniteFactor.attenuated_two_mask_integral_le line 119