The fixed scalar envelope bounds the literal lowGeometry of both source branches. Its inputs are the existing frame and neighbor costs, with no assumed estimate for the new coupling or tilt.
theorem
EulerParentRenewalScale.tilt_small_of_cost
{ι : Type u_1}
(G : EulerPacketMovingFrame.PhysicalGeometryData ι)
{cost : ℕ → ℝ}
{η : ℝ}
(n : ℕ)
(hs : EulerPacketSourceScaleChoice.SmallSeries cost η)
(hη : η ≤ 1 / 2)
(h : G.tiltError ≤ cost n)
:
theorem
EulerParentRenewalScale.literal_step
{ι : Type u_1}
{V : Type}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
{D : EulerTransversePacketProvider.Data V}
{G : EulerPacketMovingFrame.PhysicalGeometryData ι}
{Q : EulerPacketSourceGeometry.ParentFrame D G.targetTime}
(H : EulerParentPacketFrames.RenewalAtTarget G Q)
(J : ℕ)
(X : ℝ)
(n : ℕ)
{cost : ℕ → ℝ}
{η : ℝ}
(hs : EulerPacketSourceScaleChoice.SmallSeries cost η)
(hη : η ≤ 1 / 2)
(hcost : G.couplingError ≤ cost n ∧ G.tiltError ≤ cost n)
(hy : G.y = (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1))⁻¹)
:
Apply this to the matching certificate proved by either actual target-renewal constructor. It supplies exactly the finite-prefix step.
theorem
EulerPacketSourceGeometry.Guards.renewal_errors_on_scales
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{P : ParentFrame D τ}
{H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(J D0 : ℕ)
(hJ : 2 ≤ J)
(C c CF X a : ℝ)
(hC : 1 ≤ C)
(hCF : 1 ≤ CF)
(hX : 1 ≤ X)
(ha : a ≤ 2)
(n : ℕ)
(haMatch : P.a = a)
(hShear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hG : P.G ≤ CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n))
(hError : P.error ≤ EulerPacketSourceScaleActual.priorError J D0 X n)
(hNeighbor : P.neighborCost hτ hτT H A.CM A.CH * A.radius ≤ EulerPacketSourceScaleActual.neighborError J D0 X c n)
(hY : A.y = (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1))⁻¹)
(hSigma : P.sigma ^ 2 * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2)
:
(A.lowGeometry hball).couplingError ≤ EulerParentRenewalScale.renewalCost J D0 C c CF X n ∧ (A.lowGeometry hball).tiltError ≤ EulerParentRenewalScale.renewalCost J D0 C c CF X n
theorem
EulerPacketSourceGeometry.ForwardGuards.renewal_errors_on_scales
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(hball : 1 / 2 ≤ A.radius)
(J D0 : ℕ)
(hJ : 2 ≤ J)
(C c CF X a : ℝ)
(hC : 1 ≤ C)
(hCF : 1 ≤ CF)
(hX : 1 ≤ X)
(ha : a ≤ 2)
(n : ℕ)
(haMatch : P.a = a)
(hShear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hG : P.G ≤ CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n))
(hError : P.error ≤ EulerPacketSourceScaleActual.priorError J D0 X n)
(hNeighbor : ‖D.M.derivative.field‖ * A.radius ≤ EulerPacketSourceScaleActual.neighborError J D0 X c n)
(hY : A.y = (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1))⁻¹)
(hSigma : P.sigma ^ 2 * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2)
:
(A.lowGeometry hball).couplingError ≤ EulerParentRenewalScale.renewalCost J D0 C c CF X n ∧ (A.lowGeometry hball).tiltError ≤ EulerParentRenewalScale.renewalCost J D0 C c CF X n