ScalarComparison.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Signed scalar expansions preserve their coefficients through comparison.

lemma OAI.TwoPointCorrelations.uniformAverage_mul_const line 11

theorem OAI.TwoPointCorrelations.scalar_average_comparison line 19

Source documentation

Each event is compared before absolute values are taken. The total error is weighted by the absolute values of the original signed coefficients.

theorem scalar_average_comparison {α β ι : Type*}
    [Fintype α] [Fintype β] [Fintype ι]
    (f : ι → α → ℝ) (g : ι → β → ℝ) (c error : ι → ℝ)
    (h : ∀ i, |uniformAverage (f i) - uniformAverage (g i)| ≤ error i) :
    |uniformAverage (fun x => ∑ i, c i * f i x) -
      uniformAverage (fun y => ∑ i, c i * g i y)| ≤ ∑ i, |c i| * error i := by
…

Mentions: OAI.TwoPointCorrelations.uniformAverage

theorem OAI.TwoPointCorrelations.scalar_average_comparison_uniform line 35

Source documentation

Uniform event error times total absolute coefficient mass.

theorem scalar_average_comparison_uniform {α β ι : Type*}
    [Fintype α] [Fintype β] [Fintype ι]
    (f : ι → α → ℝ) (g : ι → β → ℝ) (c : ι → ℝ) (error : ℝ)
    (h : ∀ i, |uniformAverage (f i) - uniformAverage (g i)| ≤ error) :
    |uniformAverage (fun x => ∑ i, c i * f i x) -
      uniformAverage (fun y => ∑ i, c i * g i y)| ≤ (∑ i, |c i|) * error := by
…

Mentions: OAI.TwoPointCorrelations.uniformAverage