Inner product space #
In this module we define the type class InnerProductSpace' 𝕜 E which is a
generalization of InnerProductSpace 𝕜 E, as it does not require the condition ‖x‖^2 = ⟪x,x⟫
but instead the condition ∃ (c > 0) (d > 0), c • ‖x‖^2 ≤ ⟪x,x⟫ ≤ d • ‖x‖^2.
Instead E is equipped with a L₂ norm ‖x‖₂ which statifies ‖x‖₂ = √⟪x,x⟫.
This allows us to define the inner product space structure on product types E × F and
pi types ι → E, which would otherwise not be possible due to the use of max norm on these types.
We define the following maps:
InnerProductSpace 𝕜 E → InnerProductSpace' 𝕜 Ewhich sets‖x‖₂ = ‖x‖.InnerProductSpace' 𝕜 E → InnerProductSpace 𝕜 (WithLp 2 E)which uses the fact that the norm defined onWithLp 2 Eis L₂ norm.
L₂ norm on E.
In particular, on product types X×Y and pi types ι → X this class provides L₂ norm unlike ‖·‖.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Effectively as InnerProductSpace 𝕜 E but it does not requires that ‖x‖^2 = ⟪x,x⟫. It is
only required that they are equivalent ∃ (c > 0) (d > 0), c • ‖x‖^2 ≤ ⟪x,x⟫ ≤ d • ‖x‖^2. The main
purpose of this class is to provide inner product space structure on product types ExF and
pi types ι → E without using WithLp gadget.
If you want to access L₂ norm use ‖x‖₂ := √⟪x,x⟫.
This class induces InnerProductSpace 𝕜 (WithLp 2 E) which equips ‖·‖ on X with L₂ norm.
This is very useful when translating results from InnerProductSpace to InnerProductSpace'
together with toL2 : E →L[𝕜] (WithLp 2 E) and fromL2 : (WithL2 2 E) →L[𝕜] E.
In short we have these implications:
InnerProductSpace 𝕜 E → InnerProductSpace' 𝕜 E
InnerProductSpace' 𝕜 E → InnerProductSpace 𝕜 (WithLp 2 E)
The reason behind this type class is that with current mathlib design the requirement
‖x‖^2 = ⟪x,x⟫ prevents us to give inner product space structure on product type E×F and pi
type ι → E as they are equipped with max norm. One has to work with WithLp 2 (E×F) and
WithLp 2 (ι → E). This places quite a bit inconvenience on users in certain scenarios.
In particular, the main motivation behind this class is to make computations of adjFDeriv and
gradient easy.
- core : InnerProductSpace.Core 𝕜 E
Core inner product properties.
The inner product induces the L₂ norm.
- inner_top_equiv_norm : ∃ (c : ℝ) (d : ℝ), 0 < c ∧ 0 < d ∧ ∀ (x : E), c • ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 x x) ∧ RCLike.re (inner 𝕜 x x) ≤ d • ‖x‖ ^ 2
Norm induced by inner product is topologicaly equivalent to the given norm on E.
Instances
Equations
- instInnerProductSpace' = { norm₂ := fun (x : E) => ‖x‖, core := InnerProductSpace.toCore, norm₂_sq_eq_re_inner := ⋯, inner_top_equiv_norm := ⋯ }
Attach L₂ norm to WithLp 2 E
Equations
- InnerProductSpace'.toNormWithL2 = { norm := fun (x : WithLp 2 E) => √(RCLike.re (inner 𝕜 ((WithLp.equiv 2 E) x) ((WithLp.equiv 2 E) x))) }
Instances For
Attach inner product to WithLp 2 E
Equations
- InnerProductSpace'.toInnerWithL2 = { inner := fun (x y : WithLp 2 E) => inner 𝕜 ((WithLp.equiv 2 E) x) ((WithLp.equiv 2 E) y) }
Instances For
Attach normed group structure to WithLp 2 E with L₂ norm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Attach normed space structure to WithLp 2 E with L₂ norm.
Equations
- InnerProductSpace'.toNormedSpaceWithL2 = { toModule := WithLp.instModule 2 𝕜 E, norm_smul_le := ⋯ }
Instances For
Attach inner product space structure to WithLp 2 E.
Equations
- One or more equations did not get rendered due to their size.
Continuous linear map from E to WithLp 2 E.
This map is continuous because we require topological equivalence between ‖·‖ and ‖·‖₂.
Equations
- InnerProductSpace'.toL2 𝕜 = { toFun := ⇑(WithLp.equiv 2 E).symm, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
Continuous linear map from WithLp 2 E to E.
This map is continuous because we require topological equivalence between ‖·‖ and ‖·‖₂.
Equations
- InnerProductSpace'.fromL2 𝕜 = { toFun := ⇑(WithLp.equiv 2 E), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
Instances For
Continuous linear equivalence between WithLp 2 E and E under InnerProductSpace' 𝕜 E.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inner product on product types E×F defined as ⟪x,y⟫ = ⟪x.fst,y.fst⟫ + ⟪x.snd,y.snd⟫.
This is just local instance as it is superseded by the following instance for
InnerProductSpace'.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.