Shortcut instances for the normed structure of L² spaces

MeasureTheory.Lp E 2 μ is an additive subgroup of the almost-everywhere function classes, so a query such as AddCommMonoid (Lp E 2 μ) or Module ℝ (Lp E 2 μ) explores the instances of every kind of subobject, each of which re-derives structures on E, before it succeeds. The shortcuts below record the instances found.

They apply to every abbreviation of an L² space, in particular to the lifted, spatial and time L² spaces of this development, and to the continuous linear maps between two such spaces.

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instPseudoMetricSpace = inferInstance

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

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

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instNorm = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instZero = inferInstance

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

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

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instAddMonoid = inferInstance

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

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instNormedAddGroup = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instAdd = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instNormedAddCommGroup = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instNeg = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instUniformSpace = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSubNegMonoid = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSub = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instAddCommMonoid = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instAddZeroClass = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSeminormedAddGroup = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instAddGroup = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instTopologicalSpace = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSeminormedAddCommGroup = NormedAddCommGroup.toSeminormedAddCommGroup

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instMetricSpace = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instAddCommGroup = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instMulActionWithZero = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instDistribSMul = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSMulWithZero = inferInstance

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

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSMul = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instSMulZeroClass = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instDistribMulAction = inferInstance

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

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instModule = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instNormedSpace = inferInstance

@[reducible]

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

Equations

• NavierStokesAndEuler.L2Shortcut.instMulAction = inferInstance

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

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

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSMul {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : SMul ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSMul = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instMulAction {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : MulAction ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instMulAction = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instMetricSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : MetricSpace (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instMetricSpace = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSeminormedAddGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : SeminormedAddGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSeminormedAddGroup = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instAddCommGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : AddCommGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instAddCommGroup = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instContinuousNeg {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : ContinuousNeg (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSMulWithZero {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : SMulWithZero ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSMulWithZero = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSub {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : Sub (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSub = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instAdd {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : Add (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instAdd = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instAddMonoid {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : AddMonoid (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instAddMonoid = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instContinuousConstSMul {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : ContinuousConstSMul ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instModule {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : Module ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instModule = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSMulZeroClass {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : SMulZeroClass ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSMulZeroClass = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instAddGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : AddGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instAddGroup = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instDistribMulAction {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : DistribMulAction ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instDistribMulAction = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instPseudoMetricSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : PseudoMetricSpace (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instPseudoMetricSpace = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instTopologicalSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : TopologicalSpace (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instTopologicalSpace = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instContinuousAdd {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : ContinuousAdd (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instNormedAddGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instNormedAddGroup = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instZero {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : Zero (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instZero = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instUniformSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : UniformSpace (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instUniformSpace = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instNorm {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : Norm (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instNorm = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instMulActionWithZero {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : MulActionWithZero ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instMulActionWithZero = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instNormedSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instNormedSpace = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instIsBoundedSMul {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : IsBoundedSMul ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instAddZeroClass {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : AddZeroClass (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instAddZeroClass = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instIsUniformAddGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : IsUniformAddGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instNormedAddCommGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instNormedAddCommGroup = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instAddCommMonoid {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : AddCommMonoid (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instAddCommMonoid = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instContinuousSub {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : ContinuousSub (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

instance NavierStokesAndEuler.L2OperatorShortcut.instContinuousSMul {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : ContinuousSMul ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

instance NavierStokesAndEuler.L2OperatorShortcut.instIsTopologicalAddGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : IsTopologicalAddGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSeminormedAddCommGroup {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : SeminormedAddCommGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSeminormedAddCommGroup = NormedAddCommGroup.toSeminormedAddCommGroup

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instNeg {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : Neg (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instNeg = inferInstance

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instSubNegMonoid {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : SubNegMonoid (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instSubNegMonoid = inferInstance

instance NavierStokesAndEuler.L2OperatorShortcut.instNormSMulClass {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : NormSMulClass ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

@[reducible]

noncomputable instance NavierStokesAndEuler.L2OperatorShortcut.instDistribSMul {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] {β : Type u_3} {F : Type u_4} {mβ : MeasurableSpace β} {ν : MeasureTheory.Measure β} [NormedAddCommGroup F] [NormedSpace ℝ F] : DistribSMul ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 ν))

Equations

• NavierStokesAndEuler.L2OperatorShortcut.instDistribSMul = inferInstance