The same geometrically selected correction supplies the actual child's whole-horizon physical bounds and its next localized source guard.

The actual initialized packet changes the initial velocity gradient by the exponentially small early/history size plus its correction error. These are the costs needed to preserve the localized source guards.

theorem EulerPacketPhysicalLowBounds.norm_le_of_shear_error (V : Matrix) (amp δ θ ev size : ℝ) (r w : EulerSmoothLimit.Space) (hamp : 0 ≤ amp) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hsize : amp * (‖r‖ * ‖w‖) ≤ δ * size) (herr : ‖V - shearTerm amp (deriv (EulerPeriodicProfile.profile δ) θ) r w‖ ≤ ev) : ‖V‖ ≤ size + ev

theorem EulerParentPacketFrames.Evolution.exactPacket_bad_gradient_increment {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) {τ : ℝ} {hτ : 0 < τ} {hτT : τ < A.T} {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ} {H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)} (G : EulerPacketSourceGeometry.Guards hτ hτT F H) (hball : 1 / 2 ≤ G.radius) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep : ℝ) (herr : E.SourceErrors m hm J support hSupport B residual k G hball hs ev ep) (t : ↑(Set.Icc 0 A.T)) (ht : EulerPacketMovingFrame.scaledTime τ F.a F.epsilon ↑t ≤ 1) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y)) x - fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ G.hchild * G.badRatio + ev

theorem EulerParentPacketFrames.Evolution.exactPacket_initial_gradient_increment {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) {τ : ℝ} {hτ : 0 < τ} {hτT : τ < A.T} {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ} {H : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)} (G : EulerPacketSourceGeometry.Guards hτ hτT F H) (hball : 1 / 2 ≤ G.radius) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep : ℝ) (herr : E.SourceErrors m hm J support hSupport B residual k G hball hs ev ep) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (0, y)) x - fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x‖ ≤ G.hchild * G.badRatio + ev

theorem EulerParentPacketFrames.Evolution.exactForwardPacket_early_gradient_increment {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) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep : ℝ) (herr : E.ForwardSourceErrors m hm J support hSupport B residual k G hball ev ep) (t : ↑(Set.Icc 0 A.T)) (ht : EulerPacketMovingFrame.scaledTime 0 F.a F.epsilon ↑t ≤ 1) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (↑t, y)) x - fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (↑t, y)) x‖ ≤ G.hchild * G.earlyRatio + ev

theorem EulerParentPacketFrames.Evolution.exactForwardPacket_initial_gradient_increment {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) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (G : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ G.radius) (hδ : 0 < G.δ) (hδ1 : G.δ ≤ 1) (ev ep : ℝ) (herr : E.ForwardSourceErrors m hm J support hSupport B residual k G hball ev ep) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => A.exactPacketVelocity m hm J support hSupport B residual k E.inverse.field E.velocity (0, y)) x - fderiv ℝ (fun (y : EulerSmoothLimit.Space) => E.velocity (0, y)) x‖ ≤ G.hchild * G.earlyRatio + ev

The next packet's localized lower initial-gradient bounds and upper pressure bound are consequences of the exact physical estimates. The radius stays fixed, and the boundary parameter has a canonical value.

noncomputable def EulerParentPacketFrames.Evolution.joinedChildLowBounds {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field EulerPacketTerminalDatum.period A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period 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) {τ : ℝ} {hτ : 0 < τ} {hτT : τ < A.T} {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) τ} {D : EulerTransversePacketProvider.HistoryData ((A.transverseData m hm J support hSupport).initial τ hτ ⋯)} (C : EulerPacketSourceGeometry.Guards hτ hτT F D) (hball : 1 / 2 ≤ C.radius) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support) (hδ : 0 < C.δ) (hδ1 : C.δ ≤ 1) (H : LowBounds A) (ev ep CM CH : ℝ) (herr : E.SourceErrors m hm J support hSupport B residual k C hball hs ev ep) (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 * C.hchild * (C.δ * EulerPacketGeometryLowBounds.goodRatio + C.badRatio) + ep) * (A.T ^ 2 / 2) + (H.Be + (C.hchild * C.badRatio + ev)) * A.T + EulerMeanHarmonic.boundaryLocalizationC2 * (H.Bc + (C.hchild * C.badRatio + ev)) * H.r ^ 3 * A.T ≤ 1 / 2) : LowBounds (A.child G k m hgraph nextEll hnext hnext1)

Joined 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.

noncomputable def EulerParentPacketFrames.Evolution.forwardChildLowBounds {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)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field EulerPacketTerminalDatum.period A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period 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) {F : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm J support hSupport) 0} (C : EulerPacketSourceGeometry.ForwardGuards F) (hball : 1 / 2 ≤ C.radius) (hδ : 0 < C.δ) (hδ1 : C.δ ≤ 1) (H : LowBounds A) (ev ep CM CH : ℝ) (herr : E.ForwardSourceErrors m hm J support hSupport B residual k C hball ev ep) (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 * C.hchild * (C.δ * EulerPacketGeometryLowBounds.goodRatio + C.earlyRatio) + ep) * (A.T ^ 2 / 2) + (H.Be + (C.hchild * C.earlyRatio + ev)) * A.T + EulerMeanHarmonic.boundaryLocalizationC2 * (H.Bc + (C.hchild * C.earlyRatio + ev)) * H.r ^ 3 * A.T ≤ 1 / 2) : LowBounds (A.child G k m hgraph nextEll hnext hnext1)

Forward 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.

noncomputable def EulerParentPacketFrames.GeometryForwardChoice.lowBounds {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (CM CH : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) (hsmall : (I.low.K + 2 * CM * I.geometry.hchild * (I.geometry.δ * EulerPacketGeometryLowBounds.goodRatio + I.geometry.earlyRatio) + k ^ (-(1 / 4))) * (I.parent.T ^ 2 / 2) + (I.low.Be + (I.geometry.hchild * I.geometry.earlyRatio + k ^ (-(1 / 4)))) * I.parent.T + EulerMeanHarmonic.boundaryLocalizationC2 * (I.low.Bc + (I.geometry.hchild * I.geometry.earlyRatio + k ^ (-(1 / 4)))) * I.low.r ^ 3 * I.parent.T ≤ 1 / 2) : LowBounds (parent I S k hk nextEll hnext hnext1 F)

Low bounds as an element of LowBounds F.parent.

Equations

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

theorem EulerParentPacketFrames.GeometryForwardChoice.lowBounds_values {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (CM CH : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) (hsmall : (I.low.K + 2 * CM * I.geometry.hchild * (I.geometry.δ * EulerPacketGeometryLowBounds.goodRatio + I.geometry.earlyRatio) + k ^ (-(1 / 4))) * (I.parent.T ^ 2 / 2) + (I.low.Be + (I.geometry.hchild * I.geometry.earlyRatio + k ^ (-(1 / 4)))) * I.parent.T + EulerMeanHarmonic.boundaryLocalizationC2 * (I.low.Bc + (I.geometry.hchild * I.geometry.earlyRatio + k ^ (-(1 / 4)))) * I.low.r ^ 3 * I.parent.T ≤ 1 / 2) : (F.lowBounds CM CH hCM hCH hsmall).Be = I.low.Be + (I.geometry.hchild * I.geometry.earlyRatio + k ^ (-(1 / 4))) ∧ (F.lowBounds CM CH hCM hCH hsmall).Bc = I.low.Bc + (I.geometry.hchild * I.geometry.earlyRatio + k ^ (-(1 / 4))) ∧ (F.lowBounds CM CH hCM hCH hsmall).K = I.low.K + 2 * CM * I.geometry.hchild * (I.geometry.δ * EulerPacketGeometryLowBounds.goodRatio + I.geometry.earlyRatio) + k ^ (-(1 / 4)) ∧ (F.lowBounds CM CH hCM hCH hsmall).r = I.low.r ∧ (F.lowBounds CM CH hCM hCH hsmall).L = EulerMeanHarmonic.boundaryLocalizationC1 * (F.lowBounds CM CH hCM hCH hsmall).Bc + 1

theorem EulerParentPacketFrames.GeometryForwardChoice.physical_bounds {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : GeometryForwardInput U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (↑t, y)) x‖ ≤ CM + I.geometry.hchild * (EulerPacketGeometryLowBounds.goodRatio + I.geometry.earlyRatio) + k ^ (-(1 / 4)) ∧ ‖fderiv ℝ ((state I S k hk nextEll hnext hnext1 F hSym).evolution.force t) x‖ ≤ CH + 2 * CM * I.geometry.hchild * (EulerPacketGeometryLowBounds.goodRatio + I.geometry.earlyRatio) + k ^ (-(1 / 4))

noncomputable def EulerParentPacketFrames.GeometryJoinedChoice.lowBounds {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (CM CH : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) (hsmall : (I.low.K + 2 * CM * I.geometry.hchild * (I.geometry.δ * EulerPacketGeometryLowBounds.goodRatio + I.geometry.badRatio) + k ^ (-(1 / 4))) * (I.parent.T ^ 2 / 2) + (I.low.Be + (I.geometry.hchild * I.geometry.badRatio + k ^ (-(1 / 4)))) * I.parent.T + EulerMeanHarmonic.boundaryLocalizationC2 * (I.low.Bc + (I.geometry.hchild * I.geometry.badRatio + k ^ (-(1 / 4)))) * I.low.r ^ 3 * I.parent.T ≤ 1 / 2) : LowBounds (parent I S k hk nextEll hnext hnext1 F)

Low bounds as an element of LowBounds F.parent.

Equations

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

theorem EulerParentPacketFrames.GeometryJoinedChoice.lowBounds_values {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (CM CH : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) (hsmall : (I.low.K + 2 * CM * I.geometry.hchild * (I.geometry.δ * EulerPacketGeometryLowBounds.goodRatio + I.geometry.badRatio) + k ^ (-(1 / 4))) * (I.parent.T ^ 2 / 2) + (I.low.Be + (I.geometry.hchild * I.geometry.badRatio + k ^ (-(1 / 4)))) * I.parent.T + EulerMeanHarmonic.boundaryLocalizationC2 * (I.low.Bc + (I.geometry.hchild * I.geometry.badRatio + k ^ (-(1 / 4)))) * I.low.r ^ 3 * I.parent.T ≤ 1 / 2) : (F.lowBounds CM CH hCM hCH hsmall).Be = I.low.Be + (I.geometry.hchild * I.geometry.badRatio + k ^ (-(1 / 4))) ∧ (F.lowBounds CM CH hCM hCH hsmall).Bc = I.low.Bc + (I.geometry.hchild * I.geometry.badRatio + k ^ (-(1 / 4))) ∧ (F.lowBounds CM CH hCM hCH hsmall).K = I.low.K + 2 * CM * I.geometry.hchild * (I.geometry.δ * EulerPacketGeometryLowBounds.goodRatio + I.geometry.badRatio) + k ^ (-(1 / 4)) ∧ (F.lowBounds CM CH hCM hCH hsmall).r = I.low.r ∧ (F.lowBounds CM CH hCM hCH hsmall).L = EulerMeanHarmonic.boundaryLocalizationC1 * (F.lowBounds CM CH hCM hCH hsmall).Bc + 1

theorem EulerParentPacketFrames.GeometryJoinedChoice.physical_bounds {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {I : EulerPacketInitial.Input U} {S : SmoothState I.parent} {k : ℝ} {hk : EulerPacketSourceFrequency.UniversalFrequency k} {nextEll : ℝ} {hnext : 0 < nextEll} {hnext1 : nextEll ≤ 1} (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (CM CH : ℝ) (hCM : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => S.evolution.velocity (↑t, y)) x‖ ≤ CM) (hCH : ∀ (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (S.evolution.force t) x‖ ≤ CH) (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (↑t, y)) x‖ ≤ CM + I.geometry.hchild * (EulerPacketGeometryLowBounds.goodRatio + I.geometry.badRatio) + k ^ (-(1 / 4)) ∧ ‖fderiv ℝ ((state I S k hk nextEll hnext hnext1 F hSym).evolution.force t) x‖ ≤ CH + 2 * CM * I.geometry.hchild * (EulerPacketGeometryLowBounds.goodRatio + I.geometry.badRatio) + k ^ (-(1 / 4))