Lp norms #
Lp norm #
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
lpNorm_eq_sum''
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
{p : ℝ}
(hp : 0 < p)
(f : (i : ι) → α i)
:
theorem
l2Norm_sq_eq_sum
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
theorem
l2Norm_eq_sum
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
theorem
l1Norm_eq_sum
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
theorem
l0Norm_eq_card
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
‖f‖_[0] = ↑(Set.Finite.toFinset ⋯).card
theorem
lpNorm_sum_le
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
{p : ENNReal}
(hp : 1 ≤ p)
{κ : Type u_4}
(s : Finset κ)
(f : κ → (i : ι) → α i)
:
‖Finset.sum s fun (i : κ) => f i‖_[p] ≤ Finset.sum s fun (i : κ) => ‖f i‖_[p]
theorem
lpNorm_expect_le
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
{p : ENNReal}
[(i : ι) → NormedSpace ℝ (α i)]
[(i : ι) → Module ℚ≥0 (α i)]
(hp : 1 ≤ p)
{κ : Type u_4}
(s : Finset κ)
(f : κ → (i : ι) → α i)
:
‖Finset.expect s fun (i : κ) => f i‖_[p] ≤ Finset.expect s fun (i : κ) => ‖f i‖_[p]
@[simp]
theorem
lpNorm_const
{ι : Type u_1}
[Fintype ι]
{α : Type u_3}
[NormedAddCommGroup α]
{p : NNReal}
(hp : p ≠ 0)
(a : α)
:
Inner product #
def
l2Inner
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
(g : ι → 𝕜)
:
𝕜
Inner product giving rise to the L2 norm.
Equations
- l2Inner f g = Finset.sum Finset.univ fun (i : ι) => (starRingEnd 𝕜) (f i) * g i
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
l2Inner_eq_sum
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
(g : ι → 𝕜)
:
l2Inner f g = Finset.sum Finset.univ fun (i : ι) => (starRingEnd 𝕜) (f i) * g i
@[simp]
theorem
conj_l2Inner
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
(g : ι → 𝕜)
:
(starRingEnd 𝕜) (l2Inner f g) = l2Inner g f
@[simp]
theorem
l2Inner_zero_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(g : ι → 𝕜)
:
@[simp]
theorem
l2Inner_zero_right
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
:
@[simp]
theorem
l2Inner_of_isEmpty
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
[IsEmpty ι]
(f : ι → 𝕜)
(g : ι → 𝕜)
:
@[simp]
theorem
l2Inner_const_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(a : 𝕜)
(f : ι → 𝕜)
:
l2Inner (Function.const ι a) f = (starRingEnd 𝕜) a * Finset.sum Finset.univ fun (x : ι) => f x
@[simp]
theorem
l2Inner_const_right
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
(a : 𝕜)
:
l2Inner f (Function.const ι a) = (Finset.sum Finset.univ fun (x : ι) => (starRingEnd 𝕜) (f x)) * a
theorem
l2Inner_smul_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
{γ : Type u_3}
[DistribSMul γ 𝕜]
[Star γ]
[StarModule γ 𝕜]
[IsScalarTower γ 𝕜 𝕜]
(c : γ)
(f : ι → 𝕜)
(g : ι → 𝕜)
:
theorem
l2Inner_smul_right
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
{γ : Type u_3}
[DistribSMul γ 𝕜]
[Star γ]
[StarModule γ 𝕜]
[SMulCommClass γ 𝕜 𝕜]
(c : γ)
(f : ι → 𝕜)
(g : ι → 𝕜)
:
theorem
smul_l2Inner_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[CommSemiring 𝕜]
[StarRing 𝕜]
{γ : Type u_3}
[DistribSMul γ 𝕜]
[InvolutiveStar γ]
[StarModule γ 𝕜]
[IsScalarTower γ 𝕜 𝕜]
(c : γ)
(f : ι → 𝕜)
(g : ι → 𝕜)
:
theorem
l2Inner_nonneg
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[OrderedCommSemiring 𝕜]
[StarRing 𝕜]
[StarOrderedRing 𝕜]
{f : ι → 𝕜}
{g : ι → 𝕜}
(hf : 0 ≤ f)
(hg : 0 ≤ g)
:
theorem
abs_l2Inner_le_l2Inner_abs
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[LinearOrderedCommRing 𝕜]
[StarRing 𝕜]
[TrivialStar 𝕜]
{f : ι → 𝕜}
{g : ι → 𝕜}
:
theorem
l2Inner_eq_inner
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[RCLike 𝕜]
(f : ι → 𝕜)
(g : ι → 𝕜)
:
l2Inner f g = ⟪(WithLp.equiv 2 (ι → 𝕜)).symm f, (WithLp.equiv 2 (ι → 𝕜)).symm g⟫_𝕜
theorem
inner_eq_l2Inner
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[RCLike 𝕜]
(f : PiLp 2 fun (_i : ι) => 𝕜)
(g : PiLp 2 fun (_i : ι) => 𝕜)
:
⟪f, g⟫_𝕜 = l2Inner ((WithLp.equiv 2 (ι → 𝕜)) f) ((WithLp.equiv 2 (ι → 𝕜)) g)
theorem
lpNorm_translate_sum_sub_le
{α : Type u_3}
{β : Type u_4}
[AddCommGroup α]
[Fintype α]
{p : ENNReal}
[NormedAddCommGroup β]
(hp : 1 ≤ p)
{ι : Type u_5}
(s : Finset ι)
(a : ι → α)
(f : α → β)
:
The positivity extension which identifies expressions of the form ‖f‖_[p].
Instances For
The positivity extension which identifies expressions of the form ⟪f, g⟫_[𝕜].
Instances For
Hölder inequality #
theorem
lpNorm_prod_le
{ι : Type u_1}
{𝕜 : Type u_2}
{α : Type u_3}
[Fintype α]
[RCLike 𝕜]
{s : Finset ι}
(hs : s.Nonempty)
{p : ι → NNReal}
(hp : ∀ (i : ι), p i ≠ 0)
(q : NNReal)
(hpq : (Finset.sum s fun (i : ι) => (p i)⁻¹) = q⁻¹)
(f : ι → α → 𝕜)
:
‖Finset.prod s fun (i : ι) => f i‖_[↑q] ≤ Finset.prod s fun (i : ι) => ‖f i‖_[↑(p i)]
Hölder's inequality, finitary case.