One fixed coefficient radius controls both the true cover sup norms and the actual cylinder L² norms of the corrected lifted velocity.

The true lifted coefficient of an approximation plus correction has a small amplitude controlled by the scaled spatial field, the actual normal component, and the correction size.

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds1 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds1 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds2 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds2 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds3 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds3 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds4 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds4 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds5 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds5 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds6 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds6 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds7 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds7 n = inferInstance

@[instance_reducible]

noncomputable def EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds8 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerLiftedSmoothTimeField.instLiftedSmoothTimeFieldBounds8 n = inferInstance

theorem EulerLiftedSmoothTimeField.lift_add_jet_norm_le {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A B : SmoothTimeField K E EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) (n : ℕ) : ‖(lift (A.add B) κ m).jet n‖ ≤ |κ| * ‖A.jet n‖ + ‖(SmoothTimeField.map (EulerPacketCylinderField.normalComponentMap m) A).jet n‖ + (|κ| + ‖m‖) * ‖B.jet n‖

theorem EulerLiftedSmoothTimeField.lift_add_jet_bound {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A B : SmoothTimeField K E EulerSmoothLimit.Space) (κ : ℝ) (m : EulerSmoothLimit.Space) (R C0 Cn Ce : ℝ) (hA : ∀ (n : ℕ), ‖A.jet n‖ ≤ C0 * R ^ n * ↑n.factorial ^ 2) (hN : ∀ (n : ℕ), ‖(SmoothTimeField.map (EulerPacketCylinderField.normalComponentMap m) A).jet n‖ ≤ Cn * R ^ n * ↑n.factorial ^ 2) (hE : ∀ (n : ℕ), ‖B.jet n‖ ≤ Ce * R ^ n * ↑n.factorial ^ 2) (n : ℕ) : ‖(lift (A.add B) κ m).jet n‖ ≤ (|κ| * C0 + Cn + (|κ| + ‖m‖) * Ce) * R ^ n * ↑n.factorial ^ 2

theorem EulerLiftedSmoothTimeField.lift_add_inverse_scale_bound {K E : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (A B : SmoothTimeField K E EulerSmoothLimit.Space) (k : ℝ) (hk : 1 ≤ k) (m : EulerSmoothLimit.Space) (hm : ‖m‖ ≤ 1) (R C0 Cn Ce : ℝ) (hR : 0 ≤ R) (hCe : 0 ≤ Ce) (hA : ∀ (n : ℕ), ‖A.jet n‖ ≤ C0 * R ^ n * ↑n.factorial ^ 2) (hN : ∀ (n : ℕ), ‖(SmoothTimeField.map (EulerPacketCylinderField.normalComponentMap m) A).jet n‖ ≤ Cn / k * R ^ n * ↑n.factorial ^ 2) (hE : ∀ (n : ℕ), ‖B.jet n‖ ≤ Ce * R ^ n * ↑n.factorial ^ 2) (n : ℕ) : ‖(lift (A.add B) k⁻¹ m).jet n‖ ≤ ((C0 + Cn) / k + 2 * Ce) * R ^ n * ↑n.factorial ^ 2

noncomputable def EulerAllOrderDriftCorrection.liftedInputConstant (P : ℝ) [Fact (0 < P)] : ℝ

Lifted input constant, given by 1 + sobolevEmbeddingConstant P 3.

Equations

• EulerAllOrderDriftCorrection.liftedInputConstant P = 1 + EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3

noncomputable def EulerAllOrderDriftCorrection.liftedInputRadius (R ρ : ℝ) : ℝ

Lifted input radius, given by 1 + ‖coordinateEquiv.symm.toContinuousLinearMap‖ * (R + ρ⁻¹).

Equations

• EulerAllOrderDriftCorrection.liftedInputRadius R ρ = 1 + ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (R + ρ⁻¹)

theorem EulerAllOrderDriftCorrection.liftedInputConstant_one_le (P : ℝ) [Fact (0 < P)] : 1 ≤ liftedInputConstant P

theorem EulerAllOrderDriftCorrection.liftedInputConstant_embedding_le (P : ℝ) [Fact (0 < P)] : EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 ≤ liftedInputConstant P

theorem EulerAllOrderDriftCorrection.liftedInputRadius_pos (R ρ : ℝ) (hR : 0 ≤ R) (hρ : 0 < ρ) : 0 < liftedInputRadius R ρ

theorem EulerAllOrderDriftCorrection.liftedInputRadius_packet (R ρ : ℝ) (_hR : 0 ≤ R) (hρ : 0 < ρ) : ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * R ≤ liftedInputRadius R ρ

theorem EulerAllOrderDriftCorrection.liftedInputRadius_error (R ρ : ℝ) (hR : 0 ≤ R) : ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * ρ⁻¹ ≤ liftedInputRadius R ρ

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds1 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds1 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds2 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds2 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds3 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds3 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds4 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds4 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds5 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds5 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds6 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds6 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds7 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds7 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds8 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

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

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds8 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds9 {T : ℝ} (n : ℕ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds9 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds10 {T : ℝ} (n : ℕ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderDriftCorrection.instPacketLiftedCoefficientBounds10 n = inferInstance

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_jetSeries (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hG : A.approximation = G.toFieldTower) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑((liftedPacketCoefficient P B G).field t)) q n) = EulerCylinderJetLp.tensor P (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerMetricTransport.transportDirection A.κ A.direction ((correctedFieldTower P B).pointField t q)) n

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_memLp (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hG : A.approximation = G.toFieldTower) (n : ℕ) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑((liftedPacketCoefficient P B G).field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_jet_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (k R ρ C0 Cn Ce : ℝ) (hk : 1 ≤ k) (hκ : A.κ = k⁻¹) (hm : ‖A.direction‖ ≤ 1) (hR : 0 ≤ R) (hρ : 0 < ρ) (hC0 : 0 ≤ C0) (hCn : 0 ≤ Cn) (hCe : 0 ≤ Ce) (hG : G.WordBound 6 R C0 0) (hN : (G.map (EulerPacketCylinderField.normalComponentMap A.direction)).WordBound 6 R (Cn / k) 0) (hE : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((fieldTower P B).realization (n + 6)) t) ≤ Ce) (n : ℕ) : ‖(liftedPacketCoefficient P B G).jet n‖ ≤ liftedInputConstant P * ((C0 + Cn) / k + 2 * Ce) * liftedInputRadius R ρ ^ n * ↑n.factorial ^ 2

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_L2_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hGfield : A.approximation = G.toFieldTower) (k R ρ C0 Cn Ce : ℝ) (hk : 1 ≤ k) (hκ : A.κ = k⁻¹) (hm : ‖A.direction‖ ≤ 1) (hR : 0 ≤ R) (hρ : 0 < ρ) (hC0 : 0 ≤ C0) (hCn : 0 ≤ Cn) (hCe : 0 ≤ Ce) (hG : G.WordBound 6 R C0 0) (hN : (G.map (EulerPacketCylinderField.normalComponentMap A.direction)).WordBound 6 R (Cn / k) 0) (hE : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ (((fieldTower P B).realization (n + 6)) t) ≤ Ce) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑((liftedPacketCoefficient P B G).field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ liftedInputConstant P * ((C0 + Cn) / k + 2 * Ce) * liftedInputRadius R ρ ^ n * ↑n.factorial ^ 2