Cancellation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sampling_average_square_expansion line 11

Source documentation

Exact finite-average expansion, before bounding or discarding any term.

theorem sampling_average_square_expansion {ι Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (S : Finset ι) (f : ι → Ω → ℝ) (g : Ω → ℝ)
    (hpair : ∀ n ∈ S, ∀ k ∈ S, Integrable (fun x => f n x*f k x) μ)
    (hmix : ∀ n ∈ S, Integrable (fun x => f n x*g x) μ)
    (hg : Integrable (fun x => g x^2) μ) :
    (∫ x, ((∑ n ∈ S, f n x)/(S.card : ℝ)-g x)^2 ∂μ) =
      (∑ n ∈ S, ∑ k ∈ S, ∫ x, f n x*f k x ∂μ)/(S.card : ℝ)^2 -
      2*(∑ n ∈ S, ∫ x, f n x*g x ∂μ)/(S.card : ℝ)+(∫ x, g x^2 ∂μ) := by
…

theorem OAI.FiniteFactor.sampling_average_square_integrable line 43

Source documentation

Integrability of the full error follows from the same finite expansion.

theorem sampling_average_square_integrable {ι Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (S : Finset ι) (f : ι → Ω → ℝ) (g : Ω → ℝ)
    (hpair : ∀ n ∈ S, ∀ k ∈ S, Integrable (fun x => f n x*f k x) μ)
    (hmix : ∀ n ∈ S, Integrable (fun x => f n x*g x) μ)
    (hg : Integrable (fun x => g x^2) μ) :
    Integrable (fun x => ((∑ n ∈ S, f n x)/(S.card : ℝ)-g x)^2) μ := by
…

theorem OAI.FiniteFactor.sampling_finite_cancellation line 65

Source documentation

The distinct-pair and mixed main terms cancel to -A/P. Since A is nonnegative, the surviving upper bound is the actual diagonal term plus 3ε.

theorem sampling_finite_cancellation {ι : Type*} (S : Finset ι) (hS : S.Nonempty)
    (B : ι → ι → ℝ) (M : ι → ℝ) (A ε : ℝ) (hA : 0 ≤ A) (hε : 0 ≤ ε)
    (hpair : ∀ n ∈ S, ∀ k ∈ S, n ≠ k → |B n k-A| ≤ ε)
    (hmix : ∀ n ∈ S, |M n-A| ≤ ε) :
    (∑ n ∈ S, ∑ k ∈ S, B n k)/(S.card : ℝ)^2 -
      2*(∑ n ∈ S, M n)/(S.card : ℝ)+A ≤
      (∑ n ∈ S, B n n)/(S.card : ℝ)^2+3*ε := by
…