The actual stage guards satisfy the fixed pressure, initial-gradient and frame-renewal budgets used by the induction.
Actual geometric pressure increments are dominated by the literal summable scale costs. The physical parent-strain bound is CM times the previous shear, while the activation constants remain fixed low constants.
theorem
EulerParentPacketFrames.LabelData.joined_bad_pressure_cost_bound
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(A : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT))
(Ti : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(J D : ℕ)
(hJ : 3 ≤ J)
(X Cθ CM CMn CHn c : ℝ)
(hX : 1 ≤ X)
(hCθ : 1 ≤ Cθ)
(hCM : 0 ≤ CM)
(hCMn : 0 ≤ CMn)
(hCHn : 0 ≤ CHn)
(hc : 1 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4))
(n : ℕ)
(M : ℝ)
(hK : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ c)
(hTib : Ti ≤ EulerPacketSourceScaleSequence.previousShear J X n)
(hCMb : A.CM ≤ CMn)
(hCHb : A.CH ≤ CHn)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hSigma : P.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hchild : A.hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
:
2 * M * A.hchild * A.badRatio ≤ EulerPacketPressureScale.badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X) n
theorem
EulerParentPacketFrames.LabelData.joined_upper_pressure_cost_bound
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(A : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT))
(Ti : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(J D : ℕ)
(hJ : 3 ≤ J)
(X Cθ CM CMn CHn c : ℝ)
(hX : 1 ≤ X)
(hCθ : 1 ≤ Cθ)
(hCM : 0 ≤ CM)
(hCMn : 0 ≤ CMn)
(hCHn : 0 ≤ CHn)
(hc : 1 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4))
(n : ℕ)
(M : ℝ)
(hK : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ c)
(hTib : Ti ≤ EulerPacketSourceScaleSequence.previousShear J X n)
(hCMb : A.CM ≤ CMn)
(hCHb : A.CH ≤ CHn)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hSigma : P.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hchild : A.hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
(hdelta : A.δ ≤ EulerPacketSourceScaleSequence.spike J X n)
:
2 * M * A.hchild * (A.δ * EulerPacketGeometryLowBounds.goodRatio + A.badRatio) ≤ 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J (EulerPacketSourceScaleChoice.scaleSequence J X) n + EulerPacketPressureScale.badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X) n
theorem
EulerParentPacketFrames.LabelData.joined_initial_gradient_cost_bound
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(A : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT))
(Ti : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(J D : ℕ)
(hJ : 3 ≤ J)
(X Cθ CM CMn CHn c : ℝ)
(hX : 1 ≤ X)
(hCθ : 1 ≤ Cθ)
(hCM : 0 ≤ CM)
(hCMn : 0 ≤ CMn)
(hCHn : 0 ≤ CHn)
(hc : 1 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4))
(n : ℕ)
(M : ℝ)
(hK : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ c)
(hTib : Ti ≤ EulerPacketSourceScaleSequence.previousShear J X n)
(hCMb : A.CM ≤ CMn)
(hCHb : A.CH ≤ CHn)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hSigma : P.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hchild : A.hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
(hMone : 1 ≤ M)
(ev : ℝ)
:
A.hchild * A.badRatio + ev ≤ EulerPacketPressureScale.badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X) n + ev
theorem
EulerPacketSourceGeometry.ForwardGuards.earlyRatio_bound
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
:
A.earlyRatio ≤ EulerParentBadRatio.badConstant * 1 ^ EulerParentBadRatio.degree * P.horizon ^ 5 * Real.exp (-(1 / (4 * P.sigma)))
theorem
EulerPacketSourceGeometry.ForwardGuards.bad_pressure_cost_bound
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(J : ℕ)
(hJ : 3 ≤ J)
(X Cθ CM CMn CHn c : ℝ)
(hX : 1 ≤ X)
(hCθ : 1 ≤ Cθ)
(hCM : 0 ≤ CM)
(hCMn : 0 ≤ CMn)
(hCHn : 0 ≤ CHn)
(hc : 0 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(n : ℕ)
(M : ℝ)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hSigma : P.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hchild : A.hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
:
2 * M * A.hchild * A.earlyRatio ≤ EulerPacketPressureScale.badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X) n
theorem
EulerPacketSourceGeometry.ForwardGuards.upper_pressure_cost_bound
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(J : ℕ)
(hJ : 3 ≤ J)
(X Cθ CM CMn CHn c : ℝ)
(hX : 1 ≤ X)
(hCθ : 1 ≤ Cθ)
(hCM : 0 ≤ CM)
(hCMn : 0 ≤ CMn)
(hCHn : 0 ≤ CHn)
(hc : 0 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(n : ℕ)
(M : ℝ)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hSigma : P.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hchild : A.hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
(hdelta : A.δ ≤ EulerPacketSourceScaleSequence.spike J X n)
:
2 * M * A.hchild * (A.δ * EulerPacketGeometryLowBounds.goodRatio + A.earlyRatio) ≤ 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J (EulerPacketSourceScaleChoice.scaleSequence J X) n + EulerPacketPressureScale.badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X) n
theorem
EulerPacketSourceGeometry.ForwardGuards.initial_gradient_cost_bound
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(A : ForwardGuards P)
(J : ℕ)
(hJ : 3 ≤ J)
(X Cθ CM CMn CHn c : ℝ)
(hX : 1 ≤ X)
(hCθ : 1 ≤ Cθ)
(hCM : 0 ≤ CM)
(hCMn : 0 ≤ CMn)
(hCHn : 0 ≤ CHn)
(hc : 0 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(n : ℕ)
(M : ℝ)
(hTheta : P.horizon ≤ EulerPacketSourceScales.sourceTheta J Cθ (EulerPacketSourceScaleChoice.scaleSequence J X) n)
(hSigma : P.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hchild : A.hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
(hMone : 1 ≤ M)
(ev : ℝ)
:
A.hchild * A.earlyRatio + ev ≤ EulerPacketPressureScale.badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X) n + ev
theorem
EulerPacketInduction.Stage.joined_horizon_bound
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
(P.joinedFrame hn).horizon ≤ EulerPacketSourceScales.sourceTheta S.J 4 (EulerPacketSourceScaleChoice.scaleSequence S.J S.X) n
theorem
EulerPacketInduction.Stage.history_inverse_shear
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
theorem
EulerPacketInduction.Stage.joined_bad_cost
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) * (P.joinedGuards hn hq hB).hchild * (P.joinedGuards hn hq hB).badRatio ≤ EulerPacketPressureScale.badCost S.J 4 EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant 80
(EulerPacketSourceScaleChoice.scaleSequence S.J S.X) n
theorem
EulerPacketInduction.Stage.joined_initial_cost
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
(P.joinedGuards hn hq hB).hchild * (P.joinedGuards hn hq hB).badRatio + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ≤ EulerPacketInductionScales.initialIncrement S.J S.X n
theorem
EulerPacketInduction.Stage.joined_pressure_cost
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n) * (P.joinedGuards hn hq hB).hchild * ((P.joinedGuards hn hq hB).δ * EulerPacketGeometryLowBounds.goodRatio + (P.joinedGuards hn hq hB).badRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4)) ≤ EulerPacketInductionScales.pressureIncrement S.J S.X n
theorem
EulerPacketInduction.Stage.joined_renewal_errors
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
(P.joinedGeometry hn hq hB).couplingError ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 (↑q) EulerPacketLowConstants.frameConstant S.X n ∧ (P.joinedGeometry hn hq hB).tiltError ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 (↑q) EulerPacketLowConstants.frameConstant S.X n
theorem
EulerPacketInduction.Stage.forward_horizon_bound
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
:
theorem
EulerPacketInduction.Stage.forward_bad_cost
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X 0) * (P.forwardGuards hq hB).hchild * (P.forwardGuards hq hB).earlyRatio ≤ EulerPacketPressureScale.badCost S.J 4 EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant 80
(EulerPacketSourceScaleChoice.scaleSequence S.J S.X) 0
theorem
EulerPacketInduction.Stage.forward_initial_cost
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
(P.forwardGuards hq hB).hchild * (P.forwardGuards hq hB).earlyRatio + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4)) ≤ EulerPacketInductionScales.initialIncrement S.J S.X 0
theorem
EulerPacketInduction.Stage.forward_pressure_cost
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
2 * (EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X 0) * (P.forwardGuards hq hB).hchild * ((P.forwardGuards hq hB).δ * EulerPacketGeometryLowBounds.goodRatio + (P.forwardGuards hq hB).earlyRatio) + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4)) ≤ EulerPacketInductionScales.pressureIncrement S.J S.X 0
theorem
EulerPacketInduction.Stage.forward_renewal_errors
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
(P.forwardGeometry hq hB).couplingError ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 (↑q) EulerPacketLowConstants.frameConstant S.X 0 ∧ (P.forwardGeometry hq hB).tiltError ≤ EulerParentRenewalScale.renewalCost S.J S.D 4 (↑q) EulerPacketLowConstants.frameConstant S.X 0