The first stage of the actual induction is constructed from the literal compact base solution and the first same-Q packet choice.

One actual first-packet correction, its physical flow, labels and source errors. The uniform scalar frequency guard constructs the record.

The first packet preserves the exterior initial bound exactly and creates the small core used by later stages. Its pressure guard comes from the actual scalar pressure, and the exact correction adds no initial support outside the packet ball.

Exact low-order propagation for the first homogeneous packet, whose amplitude is delta times the desired initial shear.

def EulerParentPacketFrames.Evolution.HomogeneousSourceErrors {A : Parent} (E : Evolution A) {U : Type u_1} [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κ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k δ hchild : ℝ) (ξ : U) (ev ep : ℝ) : Prop

The exact source (20) errors, expressed on the same normalized packet that defines the physical child. These are precisely the two errors supplied by the same-Q packet choice.

Equations

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

theorem EulerParentPacketFrames.Evolution.homogeneousSourceErrors_of_global {A : Parent} (E : Evolution A) {U : Type u_1} [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κ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k δ hchild : ℝ) (ξ : U) (ev ep : ℝ) (herr : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k E.inverse t) x - (δ * hchild * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (E.inverse.normalized t x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) ξ (↑t) (E.inverse.normalized t x))) (((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))‖ < ev ∧ ‖fderiv ℝ (gradient (A.normalizedPacketPressure m hm J support hSupport B residual k E.inverse t)) x - (EulerPacketForwardShear.pressureCoefficient (A.transverseData m hm J support hSupport) ξ (δ * hchild) t (E.inverse.normalized t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (E.inverse.normalized t x))) • ((InnerProductSpace.rankOne ℝ) (((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))) (((A.transverseData m hm J support hSupport).normal.field t) (E.inverse.normalized t x))‖ < ep) : E.HomogeneousSourceErrors m hm J support hSupport B residual k δ hchild ξ ev ep

The literal strict errors returned by the global same-Q packet theorem imply the error record without any additional analytic bound.

theorem EulerParentPacketFrames.Evolution.exactHomogeneousPacket_low_bounds {A : Parent} (E : Evolution A) {U : Type u_1} [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κ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower EulerPacketTerminalDatum.period A.T} (B : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual EulerPacketTerminalDatum.period ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) EulerPacketTerminalDatum.period κ hκ Z R)) (k : ℝ) (hk : k * κ = 1) (δ hchild : ℝ) (ξ : U) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hhchild : 0 ≤ hchild) (ev ep CM CH Kupper : ℝ) (herr : E.HomogeneousSourceErrors m hm J support hSupport B residual k δ hchild ξ ev ep) (hsize : ∀ (s : ↑(Set.Icc 0 A.T)) (y : EulerSmoothLimit.Space), ‖((A.transverseData m hm J support hSupport).normal.field s) y‖ * ‖EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) ξ (↑s) y‖ ≤ EulerPacketFirstLowBounds.firstRatio) (hflux : ∀ (s : ↑(Set.Icc 0 A.T)) (y : EulerSmoothLimit.Space), 0 ≤ inner ℝ (((A.transverseData m hm J support hSupport).normal.field s) y) ((((A.transverseData m hm J support hSupport).M.field s) y) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) ξ (↑s) y))) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) (hCM : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM) (hCH : ‖fderiv ℝ (E.force t) x‖ ≤ CH) (hupper : ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (E.force t) x) z) z ≤ Kupper * ‖z‖ ^ 2) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y)) x‖ ≤ CM + hchild * EulerPacketFirstLowBounds.firstRatio + ev ∧ ‖fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x‖ ≤ CH + 2 * CM * (hchild * EulerPacketFirstLowBounds.firstRatio) + ep ∧ ∀ (z : EulerSmoothLimit.Space), inner ℝ ((fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => A.exactPacketPressure m hm J support hSupport B residual k E.inverse.field E.pressure (↑t, y)) x) z) z ≤ (Kupper + 2 * CM * δ * (hchild * EulerPacketFirstLowBounds.firstRatio) + ep) * ‖z‖ ^ 2

noncomputable def EulerParentPacketFrames.Evolution.firstChildLowBounds {A : Parent} (E : Evolution A) (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δ1 : δ ≤ 1) (hchild : ℝ) (hhchild : 0 ≤ hchild) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯ (EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs (δ * hchild) ⋯ N hN k hk)) (G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q (EulerPacketTerminalDatum.forwardInitializedNormalizedField (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs (δ * hchild) N k)) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (hL : H.L = 0) (hquarter : A.ell ≤ 1 / 4) (hSupportBall : support ⊆ Metric.closedBall 0 (1 / 2)) (ev ep CM CH : ℝ) (herr : E.HomogeneousSourceErrors m hm J support hSupport Q (EulerPacketTerminalDatum.forwardInitializedApproximationResidual (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs (δ * hchild) ⋯ N hN k hk) k δ hchild ξ ev ep) (hsize : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖((A.transverseData m hm J support hSupport).normal.field t) x‖ * ‖EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) ξ (↑t) x‖ ≤ EulerPacketFirstLowBounds.firstRatio) (hflux : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), 0 ≤ inner ℝ (((A.transverseData m hm J support hSupport).normal.field t) x) ((((A.transverseData m hm J support hSupport).M.field t) x) (EulerPacketForwardFactorization.canonicalVelocity (A.transverseData m hm J support hSupport) ξ (↑t) x))) (hCM : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (E.force t) x‖ ≤ CH) (hsmall : (H.K + 2 * CM * δ * (hchild * EulerPacketFirstLowBounds.firstRatio) + ep) * (A.T ^ 2 / 2) + CM * A.T + EulerMeanHarmonic.boundaryLocalizationC2 * (CM + hchild * EulerPacketFirstLowBounds.firstRatio + ev) * A.ell ^ 3 * A.T ≤ 1 / 2) : LowBounds (A.child G k m hgraph nextEll hnext hnext1)

First child low bounds as an element of LowBounds (A.child G k m hgraph nextEll hnext hnext1).

Equations

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

The first packet over the concrete base solution produces an actual smooth Euler state and its localized source bounds. All analytic input comes from the same initialized correction, graph flow, and error bounds.

The first packet's size and sign hypotheses are proved for the concrete base solution on its actual restricted horizon.

noncomputable def EulerBaseDatum.firstPacketData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerTransversePacketProvider.Data ↥FirstPlane

First packet data, given by (packetBaseParent β hβ ell hell hell1 T hT hTB).transverseData firstNormal firstNormal_unit firstFrame support compact.

Equations

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

theorem EulerBaseDatum.firstPacket_primary_size (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖((firstPacketData β hβ ell hell hell1 T hT hTB).normal.field t) x‖ * ‖EulerPacketForwardFactorization.canonicalVelocity (firstPacketData β hβ ell hell hell1 T hT hTB) firstCoordinate (↑t) x‖ ≤ EulerPacketFirstLowBounds.firstRatio

theorem EulerBaseDatum.firstPacket_primary_flux (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : 0 ≤ inner ℝ (((firstPacketData β hβ ell hell hell1 T hT hTB).normal.field t) x) ((((firstPacketData β hβ ell hell hell1 T hT hTB).M.field t) x) (EulerPacketForwardFactorization.canonicalVelocity (firstPacketData β hβ ell hell hell1 T hT hTB) firstCoordinate (↑t) x))

theorem EulerBaseDatum.packetBase_physical_strain (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (packetBaseState β hβ ell hell hell1 T hT hTB).evolution.velocity (↑t, y)) x‖ ≤ initialCoefficientCost

theorem EulerBaseDatum.packetBase_physical_force (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ ((packetBaseState β hβ ell hell hell1 T hT hTB).evolution.force t) x‖ ≤ initialCoefficientCost

theorem EulerBaseDatum.packetBaseParent_scale (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseParent β hβ ell hell hell1 T hT hTB).ell = ell

theorem EulerBaseDatum.packetBaseParent_time (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseParent β hβ ell hell hell1 T hT hTB).T = T

theorem EulerBaseDatum.packetBaseLowBounds_pressure (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseLowBounds β hβ ell hell hell1 T hT hTB).K = initialCoefficientCost

noncomputable def EulerBaseDatum.firstPacketMeanData (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerMeanPacketProvider.Data

First packet mean data, given by (packetBaseParent β hβ ell hell hell1 T hT hTB).meanData (packetBaseLowBounds β hβ ell hell hell1 T hT hTB).

Equations

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

theorem EulerBaseDatum.firstPacketAgreement (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerPacketCylinderField.SourceCoefficientAgreement (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB)

noncomputable def EulerBaseDatum.firstPacketState (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild : ℝ) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period hT (EulerPacketTerminalDatum.forwardInitializedCorrectionData (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) ⋯ N hN k hk)) (G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q (EulerPacketTerminalDatum.forwardInitializedNormalizedField (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) N k)) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k firstNormal) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (labels : EulerParentPacketFrames.LabelData ((packetBaseParent β hβ ell hell hell1 T hT hTB).child G k firstNormal hgraph nextEll hnext hnext1)) : EulerParentPacketFrames.SmoothState ((packetBaseParent β hβ ell hell hell1 T hT hTB).child G k firstNormal hgraph nextEll hnext hnext1)

First packet state as an element of SmoothState ((packetBaseParent β hβ ell hell hell1 T hT hTB).child G k firstNormal hgraph nextEll hnext hnext1).

Equations

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

noncomputable def EulerBaseDatum.firstPacketLowBounds (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild : ℝ) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (Q : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period hT (EulerPacketTerminalDatum.forwardInitializedCorrectionData (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) ⋯ N hN k hk)) (G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q (EulerPacketTerminalDatum.forwardInitializedNormalizedField (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) N k)) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k firstNormal) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (hquarter : ell ≤ 1 / 4) (hδ1 : δ ≤ 1) (hhchild : 0 ≤ hchild) (ev ep : ℝ) (herr : (packetBaseState β hβ ell hell hell1 T hT hTB).evolution.HomogeneousSourceErrors firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact Q (EulerPacketTerminalDatum.forwardInitializedApproximationResidual (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) ⋯ N hN k hk) k δ hchild firstCoordinate ev ep) (hsmall : (initialCoefficientCost + 2 * initialCoefficientCost * δ * (hchild * EulerPacketFirstLowBounds.firstRatio) + ep) * (T ^ 2 / 2) + initialCoefficientCost * T + EulerMeanHarmonic.boundaryLocalizationC2 * (initialCoefficientCost + hchild * EulerPacketFirstLowBounds.firstRatio + ev) * ell ^ 3 * T ≤ 1 / 2) : EulerParentPacketFrames.LowBounds ((packetBaseParent β hβ ell hell hell1 T hT hTB).child G k firstNormal hgraph nextEll hnext hnext1)

First packet low bounds as an element of LowBounds ((packetBaseParent β hβ ell hell hell1 T hT hTB).child G k firstNormal hgraph nextEll hnext hnext1).

Equations

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

structure EulerBaseDatum.FirstPacketChoice (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : Type

First packet choice data, collecting hn, Q, G, graph, coefficient, labels and their compatibility conditions.

• hn : 1 ≤ EulerPacketSourceFrequency.truncation k
• Q : EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period hT (EulerPacketTerminalDatum.forwardInitializedCorrectionData (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯)

  Scale parameter supplied by FirstPacketChoice.

• G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period T

  Geometric data of FirstPacketChoice, of type EulerPhysicalGraphFlowBounds.Data period T.

• graph (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftTangent) : (EulerGraphInvariantFlow.graphConstraint k firstNormal) ((self.G.A.field t) q) = 0
• coefficient : self.G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period self.Q (EulerPacketTerminalDatum.forwardInitializedNormalizedField (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) (EulerPacketSourceFrequency.truncation k) k)
• labels : EulerParentPacketFrames.LabelData ((packetBaseParent β hβ ell hell hell1 T hT hTB).child self.G k firstNormal ⋯ nextEll hnext hnext1)

  Label type supplied by FirstPacketChoice.

• label_constant : self.labels.K = k ^ 80
• displacement_bound (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖(self.G.displacementField k firstNormal ell hell t).field x‖ ≤ k ^ (-(1 / 4))
• errors : (packetBaseState β hβ ell hell hell1 T hT hTB).evolution.HomogeneousSourceErrors firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact self.Q (EulerPacketTerminalDatum.forwardInitializedApproximationResidual (firstPacketMeanData β hβ ell hell hell1 T hT hTB) (firstPacketData β hβ ell hell hell1 T hT hTB) ⋯ δ hδ firstCoordinate ⋯ (δ * hchild) ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯) k δ hchild firstCoordinate (k ^ (-(1 / 4))) (k ^ (-(1 / 4)))

theorem EulerBaseDatum.exists_firstPacketChoice (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (hδ1 : δ ≤ 1) (hh : 0 < hchild) (hfrequency : EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope (firstParameterSize T δ hchild) ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (hKk : solutionLabelConstant ≤ k) (hinv : ell⁻¹ ≤ k ^ (3 / 4)) : Nonempty (FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1)

noncomputable def EulerBaseDatum.FirstPacketChoice.parent (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) : EulerParentPacketFrames.Parent

Parent, given by (packetBaseParent β hβ ell hell hell1 T hT hTB).child F.G k firstNormal F.graph nextEll hnext hnext1.

Equations

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

noncomputable def EulerBaseDatum.FirstPacketChoice.state (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) : EulerParentPacketFrames.SmoothState (parent β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F)

State, constructed using firstPacketState.

Equations

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

theorem EulerBaseDatum.FirstPacketChoice.state_label_constant (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) : (state β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F).labels.K = k ^ 80

noncomputable def EulerBaseDatum.FirstPacketChoice.lowBounds (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hchild k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) (hquarter : ell ≤ 1 / 4) (hδ1 : δ ≤ 1) (hh : 0 ≤ hchild) (hsmall : (initialCoefficientCost + 2 * initialCoefficientCost * δ * (hchild * EulerPacketFirstLowBounds.firstRatio) + k ^ (-(1 / 4))) * (T ^ 2 / 2) + initialCoefficientCost * T + EulerMeanHarmonic.boundaryLocalizationC2 * (initialCoefficientCost + hchild * EulerPacketFirstLowBounds.firstRatio + k ^ (-(1 / 4))) * ell ^ 3 * T ≤ 1 / 2) : EulerParentPacketFrames.LowBounds (parent β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F)

Low bounds, constructed using firstPacketLowBounds.

Equations

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

The first constructed packet supplies the physical low bounds and the actual center expansion needed by the first normal stage.

The physical increment between the actual packet states has exactly the normalized packet's gradient. At the fixed center this is the same quantity used by the source error bound and geometric renewal.

theorem EulerParentPacketFrames.SmoothState.packetChild_increment_fderiv {A : Parent} (S : SmoothState A) {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (symmetry : EulerCorrectionAssembly.ParityData P (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (labels : LabelData (A.child G k m hgraph nextEll hnext hnext1)) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (S.velocityIncrement (S.packetChild m hm J support hSupport B residual V hV symmetry G hG k hk hgraph nextEll hnext hnext1 labels) ↑t) x = fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k S.evolution.inverse t) (A.ell⁻¹ • x)

theorem EulerParentPacketFrames.SmoothState.packetChild_center_error {A : Parent} (S : SmoothState A) {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (symmetry : EulerCorrectionAssembly.ParityData P (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (labels : LabelData (A.child G k m hgraph nextEll hnext hnext1)) (C : ↑(Set.Icc 0 A.T) → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (error : ℝ) (herr : ∀ (t : ↑(Set.Icc 0 A.T)), ‖fderiv ℝ (A.normalizedPacketVelocity m hm J support hSupport B residual k S.evolution.inverse t) 0 - C t‖ ≤ error) (t : ↑(Set.Icc 0 A.T)) : ‖fderiv ℝ (S.velocityIncrement (S.packetChild m hm J support hSupport B residual V hV symmetry G hG k hk hgraph nextEll hnext hnext1 labels) ↑t) 0 - C t‖ ≤ error

theorem EulerBaseDatum.FirstPacketChoice.physical_bounds {β : ℝ} {hβ : |β| ≤ 1} {ell : ℝ} {hell : 0 < ell} {hell1 : ell ≤ 1} {T : ℝ} {hT : 0 < T} {hTB : T ≤ initialTime} {δ : ℝ} {hδ : 0 < δ} {hchild k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) (hδ1 : δ ≤ 1) (hh : 0 ≤ hchild) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (state β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F).evolution.velocity (↑t, y)) x‖ ≤ initialCoefficientCost + hchild * EulerPacketFirstLowBounds.firstRatio + k ^ (-(1 / 4)) ∧ ‖fderiv ℝ ((state β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F).evolution.force t) x‖ ≤ initialCoefficientCost + 2 * initialCoefficientCost * (hchild * EulerPacketFirstLowBounds.firstRatio) + k ^ (-(1 / 4))

theorem EulerBaseDatum.FirstPacketChoice.center_error {β : ℝ} {hβ : |β| ≤ 1} {ell : ℝ} {hell : 0 < ell} {hell1 : ell ≤ 1} {T : ℝ} {hT : 0 < T} {hTB : T ≤ initialTime} {δ : ℝ} {hδ : 0 < δ} {hchild k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) (t : ↑(Set.Icc 0 T)) : ‖fderiv ℝ ((packetBaseState β hβ ell hell hell1 T hT hTB).velocityIncrement (state β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F) ↑t) 0 - (δ * hchild * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ firstNormal ((packetBaseState β hβ ell hell hell1 T hT hTB).evolution.inverse.normalized t 0))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity (firstPacketData β hβ ell hell hell1 T hT hTB) firstCoordinate (↑t) ((packetBaseState β hβ ell hell hell1 T hT hTB).evolution.inverse.normalized t 0))) (((firstPacketData β hβ ell hell hell1 T hT hTB).normal.field t) ((packetBaseState β hβ ell hell hell1 T hT hTB).evolution.inverse.normalized t 0))‖ ≤ k ^ (-(1 / 4))

Exact initial frame parameters for the first normal stage: its coupling is one, tilt is beta, and shear is the prescribed first shear.

theorem EulerBaseDatum.first_basis_cross : EulerPacketCrossProduct.cross firstNormal (EuclideanSpace.single 1 1) = EuclideanSpace.single 2 1

theorem EulerBaseDatum.first_normalizedCoupling (β : ℝ) : EulerPacketMovingFrame.normalizedCoupling (linear β) firstNormal (EuclideanSpace.single 1 1) = 1

theorem EulerBaseDatum.first_normalizedTilt (β : ℝ) : EulerPacketMovingFrame.normalizedTilt (linear β) firstNormal (EuclideanSpace.single 1 1) = β

theorem EulerBaseDatum.packetBase_centerStrain_initial (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseParent β hβ ell hell hell1 T hT hTB).centerStrain 0 = linear β

theorem EulerBaseDatum.packetBase_sourceNormal_initial (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseParent β hβ ell hell hell1 T hT hTB).sourceNormal firstNormal 0 = firstNormal

theorem EulerBaseDatum.packetBase_sourceVelocity_initial (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseParent β hβ ell hell hell1 T hT hTB).sourceVelocity firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact firstCoordinate 0 = EuclideanSpace.single 1 1

theorem EulerBaseDatum.first_frame_parameters (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (P : EulerPacketSourceGeometry.ParentFrame D 0) (hchild : ℝ) (hB : P.B 0 = (packetBaseParent β hβ ell hell hell1 T hT hTB).centerStrain 0) (hm : P.m 0 = (packetBaseParent β hβ ell hell hell1 T hT hTB).sourceNormal firstNormal 0) (hv : P.v 0 = (packetBaseParent β hβ ell hell hell1 T hT hTB).sourceVelocity firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact firstCoordinate 0) (hc : P.c = hchild) : P.a = 1 ∧ P.sigma = √β ∧ P.shear = hchild

The literal base scale constructs the first actual smooth Euler packet state and its localized source bounds.

theorem EulerBaseDatum.FirstScaleGuards.x_pos {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : 0 < X

theorem EulerBaseDatum.FirstScaleGuards.tilt_bound {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : |X ^ (-2)| ≤ 1

theorem EulerBaseDatum.FirstScaleGuards.core_pos {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : 0 < EulerPacketBaseGuardScales.baseRadius X

theorem EulerBaseDatum.FirstScaleGuards.core_one {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : EulerPacketBaseGuardScales.baseRadius X ≤ 1

theorem EulerBaseDatum.FirstScaleGuards.time_pos {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : 0 < EulerPacketBaseGuardScales.baseHorizon J X

theorem EulerBaseDatum.FirstScaleGuards.spike_pos {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : 0 < X ^ (-1010)

theorem EulerBaseDatum.FirstScaleGuards.spike_one {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : X ^ (-1010) ≤ 1

theorem EulerBaseDatum.FirstScaleGuards.shear_pos {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : 0 < X ^ 1000

theorem EulerBaseDatum.FirstScaleGuards.nextRadius_pos {J : ℕ} {X : ℝ} : 0 < EulerPacketSourceScaleSequence.supportScale J X 0

theorem EulerBaseDatum.FirstScaleGuards.nextRadius_one {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) : EulerPacketSourceScaleSequence.supportScale J X 0 ≤ 1

noncomputable def EulerBaseDatum.FirstScaleGuards.packet {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : FirstPacketChoice (X ^ (-2)) ⋯ (EulerPacketBaseGuardScales.baseRadius X) ⋯ ⋯ (EulerPacketBaseGuardScales.baseHorizon J X) ⋯ ⋯ (X ^ (-1010)) ⋯ (X ^ 1000) (X ^ D) ⋯ (EulerPacketSourceScaleSequence.supportScale J X 0) ⋯ ⋯

Packet, constructed using Classical.choice.

Equations

• H.packet hJ = Classical.choice ⋯

noncomputable def EulerBaseDatum.FirstScaleGuards.parent {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : EulerParentPacketFrames.Parent

Parent, given by (H.packet hJ).parent.

Equations

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

noncomputable def EulerBaseDatum.FirstScaleGuards.state {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : EulerParentPacketFrames.SmoothState (H.parent hJ)

State, given by (H.packet hJ).state.

Equations

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

theorem EulerBaseDatum.FirstScaleGuards.state_label {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : (H.state hJ).labels.K = (X ^ D) ^ 80

theorem EulerBaseDatum.FirstScaleGuards.parent_time {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : (H.parent hJ).T = EulerPacketBaseGuardScales.baseHorizon J X

theorem EulerBaseDatum.FirstScaleGuards.parent_scale {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : (H.parent hJ).ell = EulerPacketSourceScaleSequence.supportScale J X 0

noncomputable def EulerBaseDatum.FirstScaleGuards.lowBounds {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : EulerParentPacketFrames.LowBounds (H.parent hJ)

Low bounds, constructed using FirstPacketChoice.lowBounds.

Equations

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

theorem EulerBaseDatum.FirstScaleGuards.lowBounds_values {J D : ℕ} {X : ℝ} (H : FirstScaleGuards J D X) (hJ : 1 ≤ J) : (H.lowBounds hJ).Be = initialCoefficientCost ∧ (H.lowBounds hJ).Bc = initialCoefficientCost + X ^ 1000 * EulerPacketFirstLowBounds.firstRatio + literalInitialError D X ∧ (H.lowBounds hJ).r = EulerPacketBaseGuardScales.baseRadius X ∧ (H.lowBounds hJ).K = initialCoefficientCost + literalInitialPressureCost D X

The first actual packet has the precise initial frame parameters a=1, sigma=sqrt(beta), and the prescribed polynomial shear.

noncomputable def EulerBaseDatum.FirstPacketChoice.initialFrame {β : ℝ} {hβ : |β| ≤ 1} {ell : ℝ} {hell : 0 < ell} {hell1 : ell ≤ 1} {T : ℝ} {hT : 0 < T} {hTB : T ≤ initialTime} {δ : ℝ} {hδ : 0 < δ} {hchild k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : EulerPacketSourceGeometry.ParentFrame ((parent β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1 F).transverseData m hm R S hS) 0

Initial frame as an element of ParentFrame (F.parent.transverseData m hm R S hS) 0.

Equations

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

theorem EulerBaseDatum.FirstPacketChoice.initialFrame_parameters {β : ℝ} {hβ : |β| ≤ 1} {ell : ℝ} {hell : 0 < ell} {hell1 : ell ≤ 1} {T : ℝ} {hT : 0 < T} {hTB : T ≤ initialTime} {δ : ℝ} {hδ : 0 < δ} {hchild k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : (F.initialFrame m hm R S hS).a = 1 ∧ (F.initialFrame m hm R S hS).sigma = √β ∧ (F.initialFrame m hm R S hS).shear = hchild

theorem EulerBaseDatum.FirstPacketChoice.initialFrame_costs {β : ℝ} {hβ : |β| ≤ 1} {ell : ℝ} {hell : 0 < ell} {hell1 : ell ≤ 1} {T : ℝ} {hT : 0 < T} {hTB : T ≤ initialTime} {δ : ℝ} {hδ : 0 < δ} {hchild k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : FirstPacketChoice β hβ ell hell hell1 T hT hTB δ hδ hchild k hk nextEll hnext hnext1) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : (F.initialFrame m hm R S hS).G = 1 + initialCoefficientCost ∧ (F.initialFrame m hm R S hS).error = k ^ (-(1 / 4))

noncomputable def EulerPacketInductionScales.Scales.firstStage {c B : ℝ} (S : Scales c B) : EulerPacketInduction.Stage S 0

First stage as an element of Stage S 0.

Equations

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

theorem EulerPacketInductionScales.Scales.firstStage_time {c B : ℝ} (S : Scales c B) : S.firstStage.time = 0

theorem EulerPacketInductionScales.Scales.firstStage_horizon {c B : ℝ} (S : Scales c B) : S.firstStage.parent.T = EulerPacketBaseGuardScales.baseHorizon S.J S.X

theorem EulerPacketInductionScales.Scales.firstStage_coupling {c B : ℝ} (S : Scales c B) : S.firstStage.frame.a = 1