Shortcut instances for the Hilbert structure of L² spaces

The inner product space structure and completeness of MeasureTheory.Lp E 2 μ, registered on top of the normed-space shortcuts of L2NormedShortcuts.

instance NavierStokesAndEuler.L2Shortcut.instCompleteSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [CompleteSpace E] : CompleteSpace ↥(MeasureTheory.Lp E 2 μ)

Shortcut for the completeness of an L² space.

@[instance_reducible]

noncomputable instance NavierStokesAndEuler.L2Shortcut.instInnerProductSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : InnerProductSpace ℝ ↥(MeasureTheory.Lp E 2 μ)

Shortcut for the real inner product space structure of an L² space.

Equations

• NavierStokesAndEuler.L2Shortcut.instInnerProductSpace = inferInstance

@[instance_reducible]

noncomputable instance NavierStokesAndEuler.L2Shortcut.instInner {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Inner ℝ ↥(MeasureTheory.Lp E 2 μ)

Shortcut for the real inner product of an L² space.

Equations

• NavierStokesAndEuler.L2Shortcut.instInner = inferInstance