WeightedCauchy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The weighted Cauchy inequality used to eliminate the first label

theorem OAI.JointDickman.weighted_complex_cauchy line 12

Source documentation

The first label needs only the unit-disc bound; its multiplicativity is used solely in the preceding divisor reindexing.

theorem weighted_complex_cauchy {ι : Type*} (s : Finset ι)
    (w : ι → ℝ) (g F : ι → ℂ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hg : ∀ i ∈ s, ‖g i‖ ≤ 1) :
    ‖∑ i ∈ s, (w i : ℂ) * g i * F i‖ ^ 2 ≤
      (∑ i ∈ s, w i) * ∑ i ∈ s, w i * ‖F i‖ ^ 2 := by
…

theorem OAI.JointDickman.normalized_weighted_complex_cauchy line 30

Source documentation

Factoring a common positive normalization from the finite inequality.

theorem normalized_weighted_complex_cauchy {ι : Type*} (s : Finset ι)
    (w : ι → ℝ) (g F : ι → ℂ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hg : ∀ i ∈ s, ‖g i‖ ≤ 1) {N : ℝ} (hN : 0 ≤ N) :
    ‖(∑ i ∈ s, (w i : ℂ) * g i * F i) / (N : ℂ)‖ ^ 2 ≤
      ((∑ i ∈ s, w i) / N) * ((∑ i ∈ s, w i * ‖F i‖ ^ 2) / N) := by
…