Literal rescaling and field identities for a child packet. The physical velocity gradient and scalar-pressure Hessian retain the normalized packet's size: neither receives a negative power of ell.

noncomputable def EulerPacketPhysicalLowBounds.addVelocity (ell : ℝ) (u w : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Add velocity, given by u x+ell • w (ell⁻¹ • x).

Equations

• EulerPacketPhysicalLowBounds.addVelocity ell u w x = u x + ell • w (ell⁻¹ • x)

noncomputable def EulerPacketPhysicalLowBounds.addPressure (ell : ℝ) (p q : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) : ℝ

Add pressure, given by p x+ell^2*q (ell⁻¹ • x).

Equations

• EulerPacketPhysicalLowBounds.addPressure ell p q x = p x + ell ^ 2 * q (ell⁻¹ • x)

theorem EulerPacketPhysicalLowBounds.addVelocity_fderiv (ell : ℝ) (hell : ell ≠ 0) (u w : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hu : DifferentiableAt ℝ u x) (hw : DifferentiableAt ℝ w (ell⁻¹ • x)) : fderiv ℝ (addVelocity ell u w) x = fderiv ℝ u x + fderiv ℝ w (ell⁻¹ • x)

theorem EulerPacketPhysicalLowBounds.addPressure_gradient (ell : ℝ) (hell : ell ≠ 0) (p q : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (hp : DifferentiableAt ℝ p x) (hq : DifferentiableAt ℝ q (ell⁻¹ • x)) : gradient (addPressure ell p q) x = addVelocity ell (gradient p) (gradient q) x

theorem EulerPacketPhysicalLowBounds.addPressure_hessian (ell : ℝ) (hell : ell ≠ 0) (p q : EulerSmoothLimit.Space → ℝ) (hp : Differentiable ℝ p) (hq : Differentiable ℝ q) (x : EulerSmoothLimit.Space) (hp1 : DifferentiableAt ℝ (gradient p) x) (hq1 : DifferentiableAt ℝ (gradient q) (ell⁻¹ • x)) : fderiv ℝ (gradient (addPressure ell p q)) x = fderiv ℝ (gradient p) x + fderiv ℝ (gradient q) (ell⁻¹ • x)

noncomputable def EulerParentPacketFrames.Parent.normalizedPacketVelocity (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Normalized packet velocity, constructed using κ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerParentPacketFrames.Parent.normalizedPacketPressure (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : EulerSmoothLimit.Space → ℝ

Normalized packet pressure, given by (exactPacketOfResidual P B residual).graphPotential k t ∘ I.normalized t.

Equations

• A.normalizedPacketPressure m hm J support hSupport B residual k I t = (EulerAllOrderDriftCorrection.exactPacketOfResidual P B residual).graphPotential k t ∘ I.normalized t

theorem EulerParentPacketFrames.Parent.normalizedPacketVelocity_smooth (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ (↑⊤) (A.normalizedPacketVelocity m hm J support hSupport B residual k I t)

theorem EulerParentPacketFrames.Parent.normalizedPacketPressure_smooth (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (hk : k * κ = 1) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ (↑⊤) (A.normalizedPacketPressure m hm J support hSupport B residual k I t)

theorem EulerParentPacketFrames.Parent.exactPacketVelocity_eq_addVelocity (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.exactPacketVelocity m hm J support hSupport B residual k I.field u (↑t, x) = EulerPacketPhysicalLowBounds.addVelocity A.ell (fun (y : EulerSmoothLimit.Space) => u (↑t, y)) (A.normalizedPacketVelocity m hm J support hSupport B residual k I t) x

theorem EulerParentPacketFrames.Parent.exactPacketPressure_eq_addPressure (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (p : ℝ × EulerSmoothLimit.Space → ℝ) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : A.exactPacketPressure m hm J support hSupport B residual k I.field p (↑t, x) = EulerPacketPhysicalLowBounds.addPressure A.ell (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) (A.normalizedPacketPressure m hm J support hSupport B residual k I t) x

theorem EulerParentPacketFrames.Parent.exactPacketVelocity_fderiv (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) (hu : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => u (↑t, y)) x) : fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k I.field u (↑t, y)) x = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => u (↑t, y)) x + fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k I t) (A.ell⁻¹ • x)

theorem EulerParentPacketFrames.Parent.exactPacketPressure_hessian (A : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (k : ℝ) (I : ParticleInverse A) (hk : k * κ = 1) (p : ℝ × EulerSmoothLimit.Space → ℝ) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) (hp : Differentiable ℝ fun (y : EulerSmoothLimit.Space) => p (↑t, y)) (hp1 : DifferentiableAt ℝ (gradient fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x) : fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k I.field p (↑t, y)) x = fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x + fderiv ℝ (gradient (A.normalizedPacketPressure m hm J support hSupport B residual k I t)) (A.ell⁻¹ • x)

theorem EulerParentPacketFrames.Parent.normalizedPacketVelocity_initialized (A : Parent) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < A.T) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (α : ℝ) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketTerminalDatum.initializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk)) (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : A.normalizedPacketVelocity m hm J support hSupport Q (EulerPacketTerminalDatum.initializedApproximationResidual (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk) k I t = EulerPacketTerminalDatum.initializedExactPhysicalVelocity (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk Q t (I.normalized t)

theorem EulerParentPacketFrames.Parent.normalizedPacketPressure_initialized (A : Parent) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < A.T) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (α : ℝ) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketTerminalDatum.initializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk)) (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) : A.normalizedPacketPressure m hm J support hSupport Q (EulerPacketTerminalDatum.initializedApproximationResidual (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk) k I t = EulerPacketTerminalDatum.initializedExactPhysicalPressure (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk Q t (I.normalized t)