Actual pointwise multiplication as a bounded bilinear map Hq × L² → L².

theorem EulerSobolevL2Product.scalarProduct_memLp (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => L (↑↑(EulerCylinderSobolevSpace.value period u) x) • ↑↑v x) 2 (EulerLiftedGradientSpace.liftMeasure period)

The actual scalar-vector product belongs to L² by the proved Sobolev embedding.

noncomputable def EulerSobolevL2Product.scalarProduct (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual almost-everywhere scalar-vector product represented in cylinder L².

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSobolevL2Product.scalarProduct_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↑↑(scalarProduct period hq L u v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => L (↑↑(EulerCylinderSobolevSpace.value period u) x) • ↑↑v x

theorem EulerSobolevL2Product.scalarProduct_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ‖scalarProduct period hq L u v‖ ≤ ‖L‖ * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖u‖ * ‖v‖

The actual L² product has the quantitative bilinear bound.

theorem EulerSobolevL2Product.scalarProduct_add_right (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v w : ↥(EulerLiftedGradientSpace.LiftL2 period)) : scalarProduct period hq L u (v + w) = scalarProduct period hq L u v + scalarProduct period hq L u w

theorem EulerSobolevL2Product.scalarProduct_smul_right (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (r : ℝ) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : scalarProduct period hq L u (r • v) = r • scalarProduct period hq L u v

theorem EulerSobolevL2Product.scalarProduct_add_left (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u w : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : scalarProduct period hq L (u + w) v = scalarProduct period hq L u v + scalarProduct period hq L w v

theorem EulerSobolevL2Product.scalarProduct_smul_left (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (r : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : scalarProduct period hq L (r • u) v = r • scalarProduct period hq L u v

noncomputable def EulerSobolevL2Product.scalarProductRight (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Pointwise multiplication by an Hq scalar component is a bounded linear L² operator.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSobolevL2Product.scalarProductRight_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖scalarProductRight period hq L u‖ ≤ ‖L‖ * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * ‖u‖

noncomputable def EulerSobolevL2Product.scalarProductBilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

Actual scalar-vector multiplication, as a continuous bilinear map on the complete spaces.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerSobolevL2Product.scalarProductBilinear_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ((scalarProductBilinear period hq L) u) v = scalarProduct period hq L u v

theorem EulerSobolevL2Product.scalarProduct_translation (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (a : EulerLiftedGradientSpace.LiftDomain period) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)) : scalarProduct period hq L ((EulerCylinderSobolevSpace.sobolevTranslation period q a) u) ((EulerLiftedGradientSpace.translation period a) v) = (EulerLiftedGradientSpace.translation period a) (scalarProduct period hq L u v)

The actual product is equivariant under simultaneous cylinder translation.