Actual pointwise multiplication on the complete cylinder Sobolev spaces Hq, q≥6.

The genuine smooth product bound expressed in the complete cylinder Sobolev norm.

Actual strong product jets from the genuine Sobolev-to-L² bilinear multiplication.

Translation is strongly differentiable in the actual Sobolev topology with one more derivative.

theorem EulerCylinderSobolevSpace.sobolevTranslation_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(SobolevSpace period (q + 1))) : HasDerivAt (fun (t : ℝ) => (sobolevTranslation period q (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) ((truncateOperator period q) u)) ((derivativeOperator period q i) u) 0

Differentiating cylinder translation in Hq costs precisely one Sobolev derivative.

theorem EulerSobolevL2Product.scalarProduct_hasDerivAt (period : ℝ) [Fact (0 < period)] (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (i : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 4)) (v v' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hv : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) v) v' 0) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (EulerCylinderSobolev.standardDirection i) t)) (scalarProduct period ⋯ L ((EulerCylinderSobolevSpace.truncateOperator period 3) u) v)) (scalarProduct period ⋯ L ((EulerCylinderSobolevSpace.truncateOperator period 3) u) v' + scalarProduct period ⋯ L ((EulerCylinderSobolevSpace.derivativeOperator period 3 i) u) v) 0

Genuine L² differentiation of a pointwise product, with one Sobolev derivative on its coefficient.

noncomputable def EulerSobolevL2Product.productJet (period : ℝ) [Fact (0 < period)] (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) {v : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q v) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection q (scalarProduct period ⋯ L ((EulerCylinderSobolevSpace.restrictOperator period ⋯) u) v)

Pointwise multiplication with q+3 coefficient derivatives produces a genuine q-jet.

Equations

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

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

The output Sobolev array of an actual pointwise scalar-vector product.

Equations

• EulerSobolevL2Product.productHighLow period L u v = EulerCylinderSobolevSpace.ofJet period (EulerSobolevL2Product.productJet period L u (EulerCylinderSobolevSpace.toJet period v))

@[simp]

theorem EulerSobolevL2Product.productHighLow_value (period : ℝ) [Fact (0 < period)] (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period (productHighLow period L u v) = scalarProduct period ⋯ L ((EulerCylinderSobolevSpace.restrictOperator period ⋯) u) (EulerCylinderSobolevSpace.value period v)

Actual real and scalar-vector cylinder multiplication at every fixed Sobolev order q≥6.

theorem EulerGeneralCylinderAlgebra.real_cylinder_Hq_algebra (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerCylinderSobolev.liftSobolevNorm period q (f * g) ≤ algebraConstant period q * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

The actual real cylinder algebra estimate at every fixed order q≥6.

theorem EulerGeneralCylinderAlgebra.real_product_word_memLp (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 6 ≤ q) (hn : n ≤ q) (w : Fin n → Fin 4) (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (f * g)) 2 (EulerLiftedGradientSpace.liftMeasure period)

Every real product derivative through order q is genuinely square-integrable.

theorem EulerGeneralCylinderAlgebra.scalar_vector_product_word_memLp (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hq : 6 ≤ q) (hn : n ≤ q) (d : ℕ) (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain d) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) 2 (EulerLiftedGradientSpace.liftMeasure period)

Every scalar-vector product derivative through order q is genuinely in L².

theorem EulerGeneralCylinderAlgebra.cylinder_Hq_scalar_vector_product (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (d : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain d) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL2 : ∀ j ≤ q, ∀ (v : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period v g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (EulerCylinderSobolev.liftSobolevNorm period q fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) ≤ ↑d * algebraConstant period q * EulerCylinderSobolev.liftSobolevNorm period q f * EulerCylinderSobolev.liftSobolevNorm period q g

Multiplication of an actual vector field by a scalar field is bounded in every Hq, q≥6.

theorem EulerSobolevL2Product.sumNorm_eq_classical (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : EulerCylinderSobolevSpace.sumNorm period u = EulerCylinderSobolev.liftSobolevNorm period q f

The derivative sum of a complete Sobolev element agrees with its smooth representative.

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

Actual pointwise multiplication has the same representative at every Sobolev order.

noncomputable def EulerSobolevL2Product.sobolevProductConstant (period : ℝ) [Fact (0 < period)] (q : ℕ) : ℝ

A fixed Sobolev-order algebra constant for the complete-array norm.

Equations

• EulerSobolevL2Product.sobolevProductConstant period q = 3 * EulerGeneralCylinderAlgebra.algebraConstant period q * ↑(Fintype.card (EulerCylinderSobolevSpace.SobolevWord q)) ^ 2

theorem EulerSobolevL2Product.sobolevProductConstant_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) : 0 ≤ sobolevProductConstant period q

theorem EulerSobolevL2Product.productHighLow_representative (period : ℝ) [Fact (0 < period)] {q : ℕ} (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) : ↑↑(EulerCylinderSobolevSpace.value period (productHighLow period L u v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => L (f x) • g x

Exact smooth product representative of the actual strong product jet.

theorem EulerSobolevL2Product.productHighLow_bound_smooth (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ‖productHighLow period L u v‖ ≤ sobolevProductConstant period q * ‖(EulerCylinderSobolevSpace.restrictOperator period ⋯) u‖ * ‖v‖

The actual product jet satisfies the low-order algebra bound whenever the inputs are smooth.

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

The high-low product is additive in its first argument.

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

The high-low product is additive in its second argument.

theorem EulerSobolevL2Product.productHighLow_sub (period : ℝ) [Fact (0 < period)] {q : ℕ} (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u w : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) (v z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : productHighLow period L u v - productHighLow period L w z = productHighLow period L (u - w) v + productHighLow period L w (v - z)

Exact product difference decomposition.

Cauchy convergence of actual smooth cylinder products in the complete Sobolev space.

theorem EulerSobolevL2Product.smooth_representative_sub (period : ℝ) [Fact (0 < period)] {q : ℕ} (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hv : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period (u - v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)

Differences of actual smooth representatives remain actual smooth representatives.

theorem EulerSobolevL2Product.productHighLow_bound_of_smooth (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hv : ∃ (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ‖productHighLow period L u v‖ ≤ sobolevProductConstant period q * ‖(EulerCylinderSobolevSpace.restrictOperator period ⋯) u‖ * ‖v‖

The smooth product bound only needs the existence of the actual smooth representatives.

theorem EulerSobolevL2Product.productHighLow_dist_of_smooth (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u w : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 3))) (v z : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hw : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period w) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hv : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hz : ∃ (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period z) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : dist (productHighLow period L u v) (productHighLow period L w z) ≤ sobolevProductConstant period q * dist ((EulerCylinderSobolevSpace.restrictOperator period ⋯) u) ((EulerCylinderSobolevSpace.restrictOperator period ⋯) w) * ‖v‖ + sobolevProductConstant period q * ‖(EulerCylinderSobolevSpace.restrictOperator period ⋯) w‖ * dist v z

The genuine product difference is controlled solely in the original Sobolev topology.

theorem EulerSobolevL2Product.cauchySeq_of_product_control {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoMetricSpace X] [PseudoMetricSpace Y] [PseudoMetricSpace Z] (u : ℕ → X) (v : ℕ → Y) (p : ℕ → Z) (A B : ℝ) (hu : CauchySeq u) (hv : CauchySeq v) (h : ∀ (n m : ℕ), dist (p n) (p m) ≤ A * dist (u n) (u m) + B * dist (v n) (v m)) : CauchySeq p

A quantitative difference estimate transfers Cauchy convergence through a bilinear operation.

noncomputable def EulerSobolevL2Product.productApprox (period : ℝ) [Fact (0 < period)] (q n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Smooth products of the concrete approximations.

Equations

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

theorem EulerSobolevL2Product.productApprox_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖productApprox period q n L u v‖ ≤ sobolevProductConstant period q * ‖u‖ * ‖v‖

The actual product approximations satisfy a bound independent of the smoothing scale.

theorem EulerSobolevL2Product.productApprox_cauchy (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : CauchySeq fun (n : ℕ) => productApprox period q n L u v

Actual smooth products converge in the complete Hq topology.

theorem EulerSobolevL2Product.productApprox_value_tendsto (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : Filter.Tendsto (fun (n : ℕ) => EulerCylinderSobolevSpace.value period (productApprox period q n L u v)) Filter.atTop (nhds (scalarProduct period ⋯ L u (EulerCylinderSobolevSpace.value period v)))

The L² values of the genuine approximating products converge to the actual pointwise product.

theorem EulerSobolevL2Product.exists_sobolev_product (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ∃ (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)), EulerCylinderSobolevSpace.value period p = scalarProduct period ⋯ L u (EulerCylinderSobolevSpace.value period v) ∧ ‖p‖ ≤ sobolevProductConstant period q * ‖u‖ * ‖v‖

The actual pointwise product lies in Hq and satisfies the proved fixed-order algebra bound.

noncomputable def EulerSobolevL2Product.productHq (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The genuine product in the complete Sobolev space, uniquely determined by its L² value.

Equations

• EulerSobolevL2Product.productHq period hq L hL u v = Classical.choose ⋯

@[simp]

theorem EulerSobolevL2Product.productHq_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period (productHq period hq L hL u v) = scalarProduct period ⋯ L u (EulerCylinderSobolevSpace.value period v)

theorem EulerSobolevL2Product.productHq_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖productHq period hq L hL u v‖ ≤ sobolevProductConstant period q * ‖u‖ * ‖v‖

The algebra bound for the genuine Sobolev product.

theorem EulerSobolevL2Product.productHq_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↑↑(EulerCylinderSobolevSpace.value period (productHq period hq L hL u v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => L (↑↑(EulerCylinderSobolevSpace.value period u) x) • ↑↑(EulerCylinderSobolevSpace.value period v) x

The product is exactly pointwise multiplication almost everywhere.

theorem EulerSobolevL2Product.productHq_add_left (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u w v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : productHq period hq L hL (u + w) v = productHq period hq L hL u v + productHq period hq L hL w v

theorem EulerSobolevL2Product.productHq_smul_left (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (r : ℝ) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : productHq period hq L hL (r • u) v = r • productHq period hq L hL u v

theorem EulerSobolevL2Product.productHq_add_right (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v w : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : productHq period hq L hL u (v + w) = productHq period hq L hL u v + productHq period hq L hL u w

theorem EulerSobolevL2Product.productHq_smul_right (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (r : ℝ) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : productHq period hq L hL u (r • v) = r • productHq period hq L hL u v

noncomputable def EulerSobolevL2Product.productHqRight (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Multiplication by a Sobolev scalar component, as an actual bounded Sobolev operator.

Equations

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

theorem EulerSobolevL2Product.productHqRight_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖productHqRight period hq L hL u‖ ≤ sobolevProductConstant period q * ‖u‖

noncomputable def EulerSobolevL2Product.productHqBilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The actual complete Sobolev algebra multiplication is a continuous bilinear map.

Equations

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

@[simp]

theorem EulerSobolevL2Product.productHqBilinear_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ((productHqBilinear period hq L hL) u) v = productHq period hq L hL u v