Related estimates used together by the same construction modules.

Common compact support for the two actual initial increments after the physical spatial dilation.

theorem EulerPhysicalL2Scaling.support_in_ball_of_zero {V : Type u_1} [NormedAddCommGroup V] (f : EulerSmoothLimit.Space → V) (R : ℝ) (hz : ∀ (x : EulerSmoothLimit.Space), R < ‖x‖ → f x = 0) : tsupport f ⊆ Metric.closedBall 0 R

theorem EulerPhysicalL2Scaling.scale_support {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ell : ℝ) (hell : 0 < ell) (f : EulerSmoothLimit.Space → V) (R : ℝ) (hs : tsupport f ⊆ Metric.closedBall 0 R) : tsupport (scale ell f) ⊆ Metric.closedBall 0 (ell * R)

theorem EulerPacketInitial.high_scaled_support {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (κ k : ℝ) (m : EulerSmoothLimit.Space) (ell : ℝ) (hell : 0 < ell) (R : ℝ) (hs : support ⊆ Metric.closedBall 0 R) : tsupport (EulerPhysicalL2Scaling.scale ell fun (x : EulerSmoothLimit.Space) => high N κ (↑t) a (↑t, x, k * inner ℝ m x)) ⊆ Metric.closedBall 0 (ell * R)

theorem EulerPacketInitial.mean_scaled_support {N : ℕ} (κ k : ℝ) (m : EulerSmoothLimit.Space) (ell : ℝ) (hell : 0 < ell) (a : ℕ → EulerPacketProfileRecursion.Profile) (hs : ∀ i ≤ N, ∀ (θ : ℝ), (tsupport fun (x : EulerSmoothLimit.Space) => (a i).mean (0, x, θ)) ⊆ {x : EulerSmoothLimit.Space | ‖ell • x‖ ≤ 2}) : tsupport (EulerPhysicalL2Scaling.scale ell fun (x : EulerSmoothLimit.Space) => mean N κ 0 a (0, x, k * inner ℝ m x)) ⊆ Metric.closedBall 0 2

All actual source mean profiles have the same localized initial support. When L=0 every mean profile starts from zero.

The actual localized mean initial condition vanishes when the source boundary coefficient L is zero.

theorem EulerMeanPacketProvider.Forcing.vector_initial_zero {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hL : D.L = 0) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vector (0, x, θ) = 0

theorem EulerMeanPacketProvider.meanSolve_zero_initial (D : Data) (hL : D.L = 0) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (meanSolve D raw).1 (0, x, θ) = 0

theorem EulerPacketCylinderField.joinedSource_mean_initial_support (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hm : primary.mean = 0) (p : ℕ) (θ : ℝ) : (tsupport fun (x : EulerSmoothLimit.Space) => (joinedSourceProfiles P M D τ hτ hτT B primary p).mean (0, x, θ)) ⊆ {x : EulerSmoothLimit.Space | ‖M.ℓ • x‖ ≤ 2}

theorem EulerPacketCylinderField.joinedSource_mean_initial_zero (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (primary : EulerPacketProfileRecursion.Profile) (hprimary : ProfileRegularity P M.T ⋯ D.support primary) (hm : primary.mean = 0) (hL : M.L = 0) (p : ℕ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (joinedSourceProfiles P M D τ hτ hτT B primary p).mean (0, x, θ) = 0

theorem EulerPacketCylinderField.source_mean_initial_support (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (θ : ℝ) : (tsupport fun (x : EulerSmoothLimit.Space) => (sourceProfiles P M D I Iprimary p).mean (0, x, θ)) ⊆ {x : EulerSmoothLimit.Space | ‖M.ℓ • x‖ ≤ 2}

theorem EulerPacketCylinderField.source_mean_initial_zero (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (hL : M.L = 0) (p : ℕ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (sourceProfiles P M D I Iprimary p).mean (0, x, θ) = 0