Literal good- and bad-interval upper-Hessian costs fit the existing summable scale family. The good contribution retains its factor delta.
The actual history contribution to the early-time size ratio is polynomial in the parent labels and reciprocal history length. The good interval keeps its absolute size constant.
theorem
EulerParentPacketFrames.LabelData.initial_history_size_le_difference
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ 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)
:
EulerPacketActivationHistory.historyLabelSizeCost (G.historyOn H m hm R S hS τ hτ hτT) ≤ L.initialHistoryDifferenceScaleCost m hm R S hS H τ hτ hτT
theorem
EulerParentPacketFrames.LabelData.initial_history_size_polynomial
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ 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)
(Ti : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
:
EulerPacketActivationHistory.historyLabelSizeCost (G.historyOn H m hm R S hS τ hτ hτT) ≤ EulerParentHistoryCost.labelHistoryConstant * (1 + L.K + Ti) ^ EulerParentHistoryCost.labelHistoryPower
Envelope, given by formula (frameAmplitude K) (labelHistoryConstant*(1+K+Ti)^labelHistoryPower) Hi CM CH.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Polynomial as an element of Polynomial ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Degree, given by polynomial.natDegree.
Instances For
Bad constant, given by cutoffBound*(8232*Real.exp 9+4*boundConstant).
Equations
Instances For
theorem
EulerParentPacketFrames.LabelData.historySizeRatio_envelope
{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)
:
theorem
EulerParentPacketFrames.LabelData.historySizeRatio_polynomial
{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)
:
theorem
EulerParentPacketFrames.LabelData.badRatio_polynomial
{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)
:
Bad coefficient, given by 1+2*CM*badConstant*(4+CMn+CHn)^degree*(2*Cθ)^5.
Equations
- EulerPacketPressureScale.badCoefficient Cθ CM CMn CHn = 1 + 2 * CM * EulerParentBadRatio.badConstant * (4 + CMn + CHn) ^ EulerParentBadRatio.degree * (2 * Cθ) ^ 5
Instances For
theorem
EulerPacketPressureScale.badCost_bound
(J : ℕ)
(hJ : 3 ≤ J)
(Cθ CM CMn CHn c : ℝ)
(hθ : 1 ≤ Cθ)
(hM : 0 ≤ CM)
(hMn : 0 ≤ CMn)
(hHn : 0 ≤ CHn)
(x : ℕ → ℝ)
(hx : ∀ (n : ℕ), 1 ≤ x n)
(n : ℕ)
(M hchild r Q Θ σ : ℝ)
(hh0 : 0 ≤ hchild)
(hr0 : 0 ≤ r)
(hQ0 : 0 ≤ Q)
(hΘ0 : 0 ≤ Θ)
(hσ : 0 < σ)
(hMb : M ≤ CM * Real.exp (x n / ↑(J - 1 + n) ^ 7))
(hhb : hchild ≤ Real.exp (x n / ↑(J + n) ^ 5))
(hQ : Q ≤ (4 + CMn + CHn) * Real.exp (c * (x n / ↑(J - 1 + n) ^ 4)))
(hΘ : Θ ≤ EulerPacketSourceScales.sourceTheta J Cθ x n)
(hσx : σ * x n ≤ 2)
(hr : r ≤ EulerParentBadRatio.badConstant * Q ^ EulerParentBadRatio.degree * Θ ^ 5 * Real.exp (-(1 / (4 * σ))))
:
theorem
EulerPacketPressureScale.goodCost_bound
(J : ℕ)
(hJ : 1 ≤ J)
(X CM M δ hchild : ℝ)
(hM : 0 ≤ CM)
(hδ : 0 ≤ δ)
(hh : 0 ≤ hchild)
(hbase : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(n : ℕ)
(hMb : M ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
(hδb : δ ≤ EulerPacketSourceScaleSequence.spike J X n)
(hhb : hchild ≤ EulerPacketSourceScaleSequence.shear J X n)
:
2 * M * hchild * (δ * EulerPacketGeometryLowBounds.goodRatio) ≤ 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J (EulerPacketSourceScaleChoice.scaleSequence J X) n
theorem
EulerPacketPressureScale.parameters_le_source_exponential
(J D : ℕ)
(hJ : 3 ≤ J)
(X c : ℝ)
(hX : 1 ≤ X)
(hc : 1 ≤ c)
(hbaseH : X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7))
(hbaseK : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4))
(n : ℕ)
(K Ti Hi cm ch CMn CHn : ℝ)
(hK : K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ c)
(hTi : Ti ≤ EulerPacketSourceScaleSequence.previousShear J X n)
(hHi : Hi ≤ 1)
(hcm : cm ≤ CMn)
(hch : ch ≤ CHn)
(hMn : 0 ≤ CMn)
(hHn : 0 ≤ CHn)
: