Normalised Lp norms #
Lp norm #
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
nlpNorm_eq_expect''
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
{p : ℝ}
(hp : 0 < p)
(f : (i : ι) → α i)
:
theorem
nl2Norm_sq_eq_expect
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
theorem
nl2Norm_eq_expect
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
theorem
nl1Norm_eq_expect
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
theorem
nl0Norm_eq_card
{ι : Type u_1}
[Fintype ι]
{α : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (α i)]
(f : (i : ι) → α i)
:
‖f‖ₙ_[0] = ↑(Set.Finite.toFinset ⋯).card
Inner product #
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
nl2Inner_eq_expect
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[Semifield 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
(g : ι → 𝕜)
:
nl2Inner f g = Finset.expect Finset.univ fun (i : ι) => (starRingEnd 𝕜) (f i) * g i
@[simp]
theorem
nl2Inner_const_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[Semifield 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
(a : 𝕜)
(f : ι → 𝕜)
:
nl2Inner (Function.const ι a) f = (starRingEnd 𝕜) a * Finset.expect Finset.univ fun (x : ι) => f x
@[simp]
theorem
nl2Inner_const_right
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[Semifield 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
(f : ι → 𝕜)
(a : 𝕜)
:
nl2Inner f (Function.const ι a) = (Finset.expect Finset.univ fun (x : ι) => (starRingEnd 𝕜) (f x)) * a
theorem
nl2Inner_smul_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[Semifield 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
{γ : Type u_3}
[DistribSMul γ 𝕜]
[Star γ]
[StarModule γ 𝕜]
[SMulCommClass γ ℚ≥0 𝕜]
[IsScalarTower γ 𝕜 𝕜]
(c : γ)
(f : ι → 𝕜)
(g : ι → 𝕜)
:
theorem
nl2Inner_smul_right
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[Semifield 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
{γ : Type u_3}
[DistribSMul γ 𝕜]
[Star γ]
[StarModule γ 𝕜]
[SMulCommClass γ ℚ≥0 𝕜]
[IsScalarTower γ 𝕜 𝕜]
[SMulCommClass γ 𝕜 𝕜]
(c : γ)
(f : ι → 𝕜)
(g : ι → 𝕜)
:
theorem
smul_nl2Inner_left
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[Semifield 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
{γ : Type u_3}
[DistribSMul γ 𝕜]
[InvolutiveStar γ]
[StarModule γ 𝕜]
[SMulCommClass γ ℚ≥0 𝕜]
[IsScalarTower γ 𝕜 𝕜]
(c : γ)
(f : ι → 𝕜)
(g : ι → 𝕜)
:
theorem
nl2Inner_nonneg
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[LinearOrderedSemifield 𝕜]
[PosSMulMono ℚ≥0 𝕜]
[CharZero 𝕜]
[StarRing 𝕜]
[StarOrderedRing 𝕜]
{f : ι → 𝕜}
{g : ι → 𝕜}
(hf : 0 ≤ f)
(hg : 0 ≤ g)
:
theorem
abs_nl2Inner_le_nl2Inner_abs
{ι : Type u_1}
{𝕜 : Type u_2}
[Fintype ι]
[LinearOrderedField 𝕜]
[StarRing 𝕜]
[TrivialStar 𝕜]
{f : ι → 𝕜}
{g : ι → 𝕜}
:
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
nlpNorm_prod_le
{ι : Type u_1}
{α : Type u_3}
[Fintype α]
{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.