Actual packet matrix coefficients provide the complete coefficient towers required by the all-order nonlinear correction construction.

The constructed coefficient jets act continuously in operator norm on every finite cylinder Sobolev space.

Operator-norm continuity into a finite Sobolev space is equivalent to continuity of all its actual derivative-coordinate operators.

noncomputable def EulerCylinderSobolevSpace.wordComposition (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (q : ℕ) (A : E →L[ℝ] ↥(SobolevSpace P q)) : SobolevWord q → E →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 P)

Word composition, defined pointwise by (wordOperator P w).comp A.

Equations

• EulerCylinderSobolevSpace.wordComposition P q A w = EulerCylinderSobolevSpace.wordOperator P w ∘SL A

theorem EulerCylinderSobolevSpace.norm_wordComposition (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (q : ℕ) (A : E →L[ℝ] ↥(SobolevSpace P q)) : ‖wordComposition P q A‖ = ‖A‖

theorem EulerCylinderSobolevSpace.wordComposition_isometry (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (q : ℕ) : Isometry (wordComposition P q)

theorem EulerCylinderSobolevSpace.continuous_of_wordCompositions (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Type u_2} [TopologicalSpace K] (q : ℕ) (A : K → E →L[ℝ] ↥(SobolevSpace P q)) (hA : ∀ (w : SobolevWord q), Continuous fun (t : K) => wordOperator P w ∘SL A t) : Continuous A

theorem EulerCylinderSobolevSpace.continuous_of_valueComposition (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Type u_2} [TopologicalSpace K] (A : K → E →L[ℝ] ↥(SobolevSpace P 0)) (hA : Continuous fun (t : K) => valueOperator P 0 ∘SL A t) : Continuous A

theorem EulerCylinderSobolevSpace.continuous_of_value_and_derivatives (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Type u_2} [TopologicalSpace K] (q : ℕ) (A : K → E →L[ℝ] ↥(SobolevSpace P (q + 1))) (hA : Continuous fun (t : K) => valueOperator P (q + 1) ∘SL A t) (hD : ∀ (i : Fin 4), Continuous fun (t : K) => derivativeOperator P q i ∘SL A t) : Continuous A

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSobolev1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSobolev2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathSobolev2 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSobolev3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathSobolev3 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSobolev4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerCoefficientPath.instCoefficientPathSobolev4 = inferInstance

noncomputable def EulerCoefficientPath.sobolevOperator {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) (t : K) : ↥(EulerCylinderSobolevSpace.SobolevSpace P q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

Sobolev operator, given by coefficientSobolevOperator P (coefficientJet P A hA q t).

Equations

• EulerCoefficientPath.sobolevOperator P A hA q t = EulerSobolevCoefficientPressure.coefficientSobolevOperator P (EulerCoefficientPath.coefficientJet P A hA q t)

@[simp]

theorem EulerCoefficientPath.sobolevOperator_value {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) (t : K) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) : EulerCylinderSobolevSpace.value P ((sobolevOperator P A hA q t) u) = (smoothCoefficient P A hA t).operator (EulerCylinderSobolevSpace.value P u)

theorem EulerCoefficientPath.sobolevOperator_value_comp {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) (t : K) : EulerCylinderSobolevSpace.valueOperator P q ∘SL sobolevOperator P A hA q t = (smoothCoefficient P A hA t).operator ∘SL EulerCylinderSobolevSpace.valueOperator P q

theorem EulerCoefficientPath.sobolevOperator_derivative {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) (t : K) (i : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P (q + 1))) : (EulerCylinderSobolevSpace.derivativeOperator P q i) ((sobolevOperator P A hA (q + 1) t) u) = (sobolevOperator P A hA q t) ((EulerCylinderSobolevSpace.derivativeOperator P q i) u) + (sobolevOperator P (EulerMeanCoefficients.orbitDerivativePath A (EulerCylinderSobolev.standardDirection i).1) ⋯ q t) ((EulerCylinderSobolevSpace.truncateOperator P q) u)

theorem EulerCoefficientPath.sobolevOperator_derivative_comp {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) (t : K) (i : Fin 4) : EulerCylinderSobolevSpace.derivativeOperator P q i ∘SL sobolevOperator P A hA (q + 1) t = sobolevOperator P A hA q t ∘SL EulerCylinderSobolevSpace.derivativeOperator P q i + sobolevOperator P (EulerMeanCoefficients.orbitDerivativePath A (EulerCylinderSobolev.standardDirection i).1) ⋯ q t ∘SL EulerCylinderSobolevSpace.truncateOperator P q

theorem EulerCoefficientPath.sobolevOperator_continuous {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) : Continuous fun (t : K) => sobolevOperator P A hA q t

noncomputable def EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) : EulerAllOrderCorrectionData.CoefficientTower P T

To coefficient tower, bundling coefficient, jet, continuous.

Equations

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

@[simp]

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_coefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ((toCoefficientTower P A).coefficient t).coefficient x = (A.path t) x.1

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_raw (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : ((toCoefficientTower P A).coefficient t).coefficient (x, ↑θ) = raw (↑t, x, θ)

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_operator (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (t : ↑(Set.Icc 0 T)) : ((toCoefficientTower P A).coefficient t).operator = (EulerLpCylinderRectangular.fullOperatorMap P) (A.path t)

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_operator_continuous (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) : Continuous fun (t : ↑(Set.Icc 0 T)) => ((toCoefficientTower P A).coefficient t).operator

theorem EulerPacketCylinderField.MatrixCoefficient.toCoefficientTower_sobolev_value (P : ℝ) [Fact (0 < P)] {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T raw) (q : ℕ) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P q)) : EulerCylinderSobolevSpace.value P ((EulerSobolevCoefficientPressure.coefficientSobolevOperator P ((toCoefficientTower P A).jet q t)) u) = ((EulerLpCylinderRectangular.fullOperatorMap P) (A.path t)) (EulerCylinderSobolevSpace.value P u)