Supported, zero-mean raw cylinder witnesses feed the actual high-mode solver.

Genuine nonlinear cylinder products preserve support of their multiplying factor.

noncomputable def EulerCylinderPathProduct.supportedPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (h : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) : C(K, ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))

Retain the actual values of a continuous path that already has the stated support.

Equations

• EulerCylinderPathProduct.supportedPath P S hS p h = { toFun := fun (t : K) => ⟨p t, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem EulerCylinderPathProduct.include_supportedPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (h : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) : (EulerLpCylinderPaths.includePath P S hS) (supportedPath P S hS p h) = p

theorem EulerCylinderPathProduct.scalarProductPath_supported_left (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) : (scalarProductPath P L hL p q hp hq) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerCylinderPathProduct.scalarProductPath_supported_right (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (hs : ∀ (t : K), q t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) : (scalarProductPath P L hL p q hp hq) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerCylinderPathProduct.bilinearProductPath_supported_left (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) : (bilinearProductPath P B p q hp hq) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerCylinderPathProduct.scalarDerivativeProductPath_supported (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (i : Fin 4) (t : K) : (scalarDerivativeProductPath P L hL p q hp hq i) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

theorem EulerCylinderPathProduct.advectionPath_supported (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (hs : ∀ (t : K), p t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS) (t : K) : (advectionPath P p q hp hq) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS

noncomputable def EulerPacketCylinderField.Field.transverseForcing {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P D.T raw) (hs : ∀ (t : ↑(Set.Icc 0 D.T)), G.path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯) (hm : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) : EulerTransversePacketProvider.Forcing P D raw

Only actual support and literal mean zero are added to the existing field witness.

Equations

• EulerPacketCylinderField.Field.transverseForcing D G hs hm = { path := EulerCylinderPathProduct.supportedPath P D.support ⋯ G.path hs, path_orbit := ⋯, raw_eq := ⋯, mean_zero := ⋯ }

noncomputable def EulerPacketCylinderField.Field.transverseForcingOfRaw {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P D.T raw) (hs : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∉ D.support, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (hm : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, raw (↑t, x, θ) = 0) : EulerTransversePacketProvider.Forcing P D raw

A literal compact-support proof may be used directly, without selecting a new representative.

Equations

• EulerPacketCylinderField.Field.transverseForcingOfRaw D G hs hm = EulerPacketCylinderField.Field.transverseForcing D G ⋯ hm