LeanPool.NavierStokesAndEuler.Euler.PacketCylinderWeightedAdvection

Same-radius normalized bounds for the literal slow and fast packet jet expressions.

Products of actual normalized fields use only the pointwise ratio of their time profiles.

noncomputable def EulerPacketCylinderField.productProfileRatio {K : Type u_1} [TopologicalSpace K] (g h b : C(K, ℝ )) (hb : ∀ (t : K), 0 < b t) :

C(K, ℝ )

Product profile ratio, given by ⟨fun t => g t*h t/b t,(g.continuous.mul h.continuous).div b.continuous (fun t => (hb t).ne')⟩.

Equations

EulerPacketCylinderField.productProfileRatio g h b hb = { toFun := fun (t : K) => g t * h t / b t, continuous_toFun := ⋯ }

Instances For

source

@[simp]

theorem EulerPacketCylinderField.productProfileRatio_apply {K : Type u_1} [TopologicalSpace K] (g h b : C(K, ℝ )) (hb : ∀ (t : K), 0 < b t) (t : K) :

(productProfileRatio g h b hb) t = g t * h t / b t

source

theorem EulerPacketCylinderField.productProfileRatio_abs_le {K : Type u_1} [TopologicalSpace K] (g h b : C(K, ℝ )) (hg : ∀ (t : K), 0 ≤ g t) (hh : ∀ (t : K), 0 ≤ h t) (hb : ∀ (t : K), 0 < b t) (C : ℝ) (hC : ∀ (t : K), g t * h t ≤ C * b t) (t : K) :

|(productProfileRatio g h b hb) t| ≤ C

source

theorem EulerPacketCylinderField.Field.normalized_bilinear_path {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) (L : EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space) :

((G.bilinear H L).normalized hT b hb).path = (((G.normalized hT g hg).bilinear (H.normalized hT h hh) L).weighted hT (productProfileRatio g h b hb)).path

source

theorem EulerPacketCylinderField.Field.normalized_scalarProduct_path {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) (L : EulerSmoothLimit.Space →L[ℝ ] ℝ) (hL : ‖L‖ ≤ 1) :

((G.scalarProduct H L hL).normalized hT b hb).path = (((G.normalized hT g hg).scalarProduct (H.normalized hT h hh) L hL).weighted hT (productProfileRatio g h b hb)).path

source

theorem EulerPacketCylinderField.Field.normalized_spatialTransport_path {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) :

((G.spatialTransport H).normalized hT b hb).path = (((G.normalized hT g hg).spatialTransport (H.normalized hT h hh)).weighted hT (productProfileRatio g h b hb)).path

source

theorem EulerPacketCylinderField.Field.WordBound.normalized_bilinear {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} (hT : 0 ≤ T) {g h b : C(↑(Set.Icc 0 T), ℝ )} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t} {hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t} {R A B : ℝ} {d e : ℕ} (hG : (G.normalized hT g hg).WordBound 6 R A d) (hH : (H.normalized hT h hh).WordBound 6 R B e) (L : EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (C : ℝ) (hC : 0 ≤ C) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), |(productProfileRatio g h b hb) t| ≤ C) :

((G.bilinear H L).normalized hT b hb).WordBound 6 R (C * (9 * EulerCylinderPathProduct.productBlockConstant P * ‖L‖ * A * B)) (d + e)

source

theorem EulerPacketCylinderField.Field.WordBound.normalized_scalarProduct {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} (hT : 0 ≤ T) {g h b : C(↑(Set.Icc 0 T), ℝ )} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t} {hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t} {R A B : ℝ} {d e : ℕ} (hG : (G.normalized hT g hg).WordBound 6 R A d) (hH : (H.normalized hT h hh).WordBound 6 R B e) (L : EulerSmoothLimit.Space →L[ℝ ] ℝ) (hL : ‖L‖ ≤ 1) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (C : ℝ) (hC : 0 ≤ C) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), |(productProfileRatio g h b hb) t| ≤ C) :

((G.scalarProduct H L hL).normalized hT b hb).WordBound 6 R (C * (3 * EulerCylinderPathProduct.productBlockConstant P * A * B)) (d + e)

source

theorem EulerPacketCylinderField.Field.WordBound.normalized_spatialTransport {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} (hT : 0 ≤ T) {g h b : C(↑(Set.Icc 0 T), ℝ )} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t} {hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t} {R A B : ℝ} {d e : ℕ} (hG : (G.normalized hT g hg).WordBound 6 R A d) (hH : (H.normalized hT h hh).WordBound 6 R B e) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (C : ℝ) (hC : 0 ≤ C) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), |(productProfileRatio g h b hb) t| ≤ C) :

((G.spatialTransport H).normalized hT b hb).WordBound 6 R (C * (9 * EulerCylinderPathProduct.productBlockConstant P * A * B)) (d + e + 1)

source

theorem EulerPacketCylinderField.SpatialJetField.slowAdvection_normalized_bound {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {inverse : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space} (F : MatrixCoefficient T inverse) {R A B : ℝ} {d e : ℕ} (hG : (G.field.normalized hT g hg).WordBound 6 R A d) (hH : (H.field.normalized hT h hh).WordBound 6 R B e) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hRF : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hF : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath F.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (c : ℝ) (hc : 0 ≤ c) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), |(productProfileRatio g h b hb) t| ≤ c) :

((slowAdvection F G H).normalized hT b hb).WordBound 6 R (c * (9 * EulerCylinderPathProduct.productBlockConstant P * (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 Rc C * A) * B)) (d + e + 1)

source

theorem EulerPacketCylinderField.SpatialJetField.fastAdvection_normalized_bound {P T : ℝ} [Fact (0 < P)] {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) (hT : 0 ≤ T) (g h b : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hh : ∀ (t : ↑(Set.Icc 0 T)), 0 < h t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {normal : EulerPacketProfileRecursion.VectorField} (N : VectorCoefficient T normal) {R A B : ℝ} {d e : ℕ} (hG : (G.field.normalized hT g hg).WordBound 6 R A d) (hH : (H.field.normalized hT h hh).WordBound 6 R B e) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hRN : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hN : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath N.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (c : ℝ) (hc : 0 ≤ c) (hprofile : ∀ (t : ↑(Set.Icc 0 T)), |(productProfileRatio g h b hb) t| ≤ c) :

((fastAdvection N G H).normalized hT b hb).WordBound 6 R (c * (3 * EulerCylinderPathProduct.productBlockConstant P * (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 Rc C * A) * B)) (d + e + 1)

source

theorem EulerPacketCylinderField.Field.WordBound.normalized_slowPressure {P T : ℝ} [Fact (0 < P)] (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {inverse : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space} (F : MatrixCoefficient T inverse) (p : EulerPacketProfileRecursion.ScalarField) (G : Field P T (pressureGradient p)) {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hRF : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hF : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath F.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) :

((slowPressure F p G).normalized hT g hg).WordBound q R (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * A) d

source

theorem EulerPacketCylinderField.Field.WordBound.normalized_linearPart {P T : ℝ} [Fact (0 < P)] (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ )) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {strain : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ ] EulerSmoothLimit.Space} (M : MatrixCoefficient T strain) {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hTpos : 0 < T) (hd : TimeDerivative ⋯ G H) (s : Set ℝ) (hs : s = Set.Icc 0 T) {q d : ℕ} {R A B : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (hH : (H.normalized hT g hg).WordBound q R B d) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hRM : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hM : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath M.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) :

((linearPart M G H hTpos hd s hs).normalized hT g hg).WordBound q R (B + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * A) d