LeanPool.NavierStokesAndEuler.Euler.TransversePacketHomogeneity

Exact homogeneity of admissible forcing and the actual joined inverse. This permits one fixed unit-amplitude radius budget for every recursive forcing amplitude, including zero.

Exact scalar homogeneity of the constructed history and forward paths.

source

theorem EulerCylinderDirichlet.Coefficients.continuousVelocity_smul (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) :

(velocityPath P D) (EulerTimeLp.pathLp T ⋯ (a • f)) = a • (velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)

source

theorem EulerCylinderDirichlet.Coefficients.accelerationPath_smul (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) :

accelerationPath P D (a • f) = a • accelerationPath P D f

source

theorem EulerCylinderDirichlet.Coefficients.physicalVelocity_smul (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) :

physicalVelocity P D (a • f) = a • physicalVelocity P D f

source

theorem EulerCylinderDirichlet.Coefficients.physicalDerivative_smul (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) :

physicalDerivative P D (a • f) = a • physicalDerivative P D f

source

theorem EulerSourceCylinderEquation.coordinates_smul (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) :

coordinates P S hS T hT Q Q₁ c hc hQ (a • f) (a • a₀) = a • coordinates P S hS T hT Q Q₁ c hc hQ f a₀

source

theorem EulerSourceCylinderEquation.velocity_smul (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) :

velocity P S hS T hT Q Q₁ c hc hQ (a • f) (a • a₀) = a • velocity P S hS T hT Q Q₁ c hc hQ f a₀

source

theorem EulerSourceCylinderEquation.velocityDerivative_smul (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (a : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) :

velocityDerivative P S hS T hT Q Q₁ c hc hQ (a • f) (a • a₀) = a • velocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀

source

noncomputable def EulerTransversePacketProvider.Forcing.smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (a : ℝ) :

Forcing P D (a • raw)

Scalar multiplication of the literal forcing, with its genuine path witness.

Equations

G.smul a = { path := a • G.path, path_orbit := ⋯, raw_eq := ⋯, mean_zero := ⋯ }

Instances For

source

theorem EulerTransversePacketProvider.Forcing.velocityPath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (H : Forcing P D raw') (I J : InitialData P D) (a : ℝ) (h : H.path = a • G.path) (hi : J.value = a • I.value) :

H.velocityPath J = a • G.velocityPath I

source

theorem EulerTransversePacketProvider.Forcing.derivativePath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (H : Forcing P D raw') (I J : InitialData P D) (a : ℝ) (h : H.path = a • G.path) (hi : J.value = a • I.value) :

H.derivativePath J = a • G.derivativePath I

source

theorem EulerTransversePacketProvider.HistoryData.coordinatePath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (H : Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

B.coordinatePath H = a • B.coordinatePath G

source

theorem EulerTransversePacketProvider.HistoryData.velocityPath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (H : Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

B.velocityPath H = a • B.velocityPath G

source

theorem EulerTransversePacketProvider.HistoryData.derivativePath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (H : Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

B.derivativePath H = a • B.derivativePath G

source

theorem EulerElapsedTimePathGluing.join_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) (a : ℝ) :

join S τ hτ hτS (a • u) (a • v) ⋯ = a • join S τ hτ hτS u v hm

source

theorem EulerTransversePacketJoin.initial_forcing_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

(H.initial τ hτ ⋯).path = a • (G.initial τ hτ ⋯).path

source

theorem EulerTransversePacketJoin.tail_forcing_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

(H.tail τ ⋯ hτT).path = a • (G.tail τ ⋯ hτT).path

source

theorem EulerTransversePacketJoin.forwardInitial_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

(forwardInitial τ hτ hτT B H).value = a • (forwardInitial τ hτ hτT B G).value

source

theorem EulerTransversePacketJoin.pastVelocity_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

pastVelocity τ hτ hτT B H = a • pastVelocity τ hτ hτT B G

source

theorem EulerTransversePacketJoin.pastDerivative_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

pastDerivative τ hτ hτT B H = a • pastDerivative τ hτ hτT B G

source

theorem EulerTransversePacketJoin.futureVelocity_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

futureVelocity τ hτ hτT B H = a • futureVelocity τ hτ hτT B G

source

theorem EulerTransversePacketJoin.futureDerivative_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

futureDerivative τ hτ hτT B H = a • futureDerivative τ hτ hτT B G

source

theorem EulerTransversePacketJoin.velocityPath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

velocityPath τ hτ hτT B H = a • velocityPath τ hτ hτT B G

source

theorem EulerTransversePacketJoin.derivativePath_eq_smul {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw raw' : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (H : EulerTransversePacketProvider.Forcing P D raw') (a : ℝ) (h : H.path = a • G.path) :

derivativePath τ hτ hτT B H = a • derivativePath τ hτ hτT B G