Source indexedlemma · leanprover/lean4:v4.32.0

RCLike.wInner_cWeight_le_cL2Norm_mul_cL2Norm

APAP.Prereqs.Inner.Hoelder.Compact · APAP/Prereqs/Inner/Hoelder/Compact.lean:37 to 44

Source documentation

Cauchy-Schwarz inequality

Exact Lean statement

lemma wInner_cWeight_le_cL2Norm_mul_cL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2]

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma wInner_cWeight_le_cL2Norm_mul_cL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by  simp only [wInner_cWeight_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul ℝ≥0, NNRat.cast_inv,    NNRat.cast_natCast, NNReal.smul_def, NNReal.coe_inv, NNReal.coe_natCast, smul_eq_mul,    cL2Norm_eq_expect_norm, expect, card_univ, norm_eq_abs, sq_abs]  rw [mul_rpow, mul_rpow, mul_mul_mul_comm, ← sq, ← rpow_two, rpow_inv_rpow]  any_goals positivity  gcongr  simpa [dL2Norm_eq_sum_norm] using wInner_one_le_dL2Norm_mul_dL2Norm f g