Fixed summable envelopes for actual geometric renewal. The analytic envelope uses the constant sequence a=2, so its summability does not assume bounds for the future, not-yet-constructed geometric couplings.

noncomputable def EulerParentRenewalScale.maximumError (J D : ℕ) (C c X : ℝ) : ℕ → ℝ

Maximum error, given by geometryErrorCost J D C c X (fun _ => 2).

Equations

• EulerParentRenewalScale.maximumError J D C c X = EulerPacketSourceScaleActual.geometryErrorCost J D C c X fun (x : ℕ) => 2

noncomputable def EulerParentRenewalScale.errorConstant (CF : ℝ) : ℝ

Error constant, given by 30000000*neighborStabilityConstant*CF^2.

Equations

• EulerParentRenewalScale.errorConstant CF = 30000000 * EulerPacketMovingFrame.neighborStabilityConstant * CF ^ 2

noncomputable def EulerParentRenewalScale.renewalCost (J D : ℕ) (C c CF X : ℝ) (n : ℕ) : ℝ

Renewal cost, given by 3000/scaleSequence J X n+errorConstant CF*maximumError J D C c X n.

Equations

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

theorem EulerParentRenewalScale.errorConstant_nonneg (CF : ℝ) : 0 ≤ errorConstant CF

theorem EulerParentRenewalScale.maximumError_series {J D : ℕ} {C c X δ : ℝ} (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) : EulerPacketSourceScaleChoice.SmallSeries (maximumError J D C c X) δ

theorem EulerParentRenewalScale.scaleSequence_double (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 0 < X) (n : ℕ) : 2 * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ EulerPacketSourceScaleChoice.scaleSequence J X (n + 1)

theorem EulerParentRenewalScale.reciprocal_geometric (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 0 < X) (n : ℕ) : 1 / EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 1 / X * (1 / 2) ^ n

theorem EulerParentRenewalScale.reciprocal_series (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 0 < X) : EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => 1 / EulerPacketSourceScaleChoice.scaleSequence J X n) (2 / X)

theorem EulerParentRenewalScale.scale_series {f : ℕ → ℝ} {δ : ℝ} (hf : EulerPacketSourceScaleChoice.SmallSeries f δ) (C : ℝ) (hC : 0 ≤ C) : EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => C * f n) (C * δ)

theorem EulerParentRenewalScale.renewal_series {J D : ℕ} (hJ : 2 ≤ J) {C c CF X δ : ℝ} (hX : 0 < X) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) : EulerPacketSourceScaleChoice.SmallSeries (renewalCost J D C c CF X) (6000 / X + errorConstant CF * δ)

theorem EulerParentRenewalScale.renewal_series_small {J D : ℕ} (hJ : 2 ≤ J) {C c CF X δ η : ℝ} (hX : 0 < X) (hδ : 0 ≤ δ) (hη : 0 < η) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (hfloor : 12000 / η ≤ X) (hsmall : 2 * (1 + errorConstant CF) * δ ≤ η) : EulerPacketSourceScaleChoice.SmallSeries (renewalCost J D C c CF X) η

Enlarge only the final base scale; the starting index and every previously chosen cost specification remain unchanged.

theorem EulerParentRenewalScale.physical_error_le_maximum {ι : Type u_1} (G : EulerPacketMovingFrame.PhysicalGeometryData ι) (J D : ℕ) (hJ : 1 ≤ J) (C c CF X a : ℝ) (hC : 1 ≤ C) (hCF : 1 ≤ CF) (hX : 1 ≤ X) (ha : a ≤ 2) (n : ℕ) (heps : G.ε = EulerPacketSourceScaleActual.epsilon J X a n) (htheta : G.Θ ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n) (hG : G.G ≤ CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n)) (hd : G.d ≤ EulerPacketSourceScaleActual.priorError J D X n + EulerPacketSourceScaleActual.neighborError J D X c n) : G.error * G.Θ ^ 40 ≤ CF ^ 2 * maximumError J D C c X n

This uses only the coupling at the present stage.

theorem EulerParentRenewalScale.coupling_polynomial_le {ι : Type u_1} (G : EulerPacketMovingFrame.PhysicalGeometryData ι) : G.y ^ 4 + G.σ ^ 2 * G.y ^ 2 + 8 * G.σ * G.y ^ 3 ≤ 10 * G.y

theorem EulerParentRenewalScale.actual_errors_le_cost {ι : Type u_1} (G : EulerPacketMovingFrame.PhysicalGeometryData ι) (J D : ℕ) (hJ : 2 ≤ J) (C c CF X a : ℝ) (hC : 1 ≤ C) (hCF : 1 ≤ CF) (hX : 1 ≤ X) (ha : a ≤ 2) (n : ℕ) (heps : G.ε = EulerPacketSourceScaleActual.epsilon J X a n) (htheta : G.Θ ≤ EulerPacketSourceScales.sourceTheta J C (EulerPacketSourceScaleChoice.scaleSequence J X) n) (hG : G.G ≤ CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n)) (hd : G.d ≤ EulerPacketSourceScaleActual.priorError J D X n + EulerPacketSourceScaleActual.neighborError J D X c n) (hy : G.y = (EulerPacketSourceScaleChoice.scaleSequence J X (n + 1))⁻¹) (hsigma : G.σ * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2) : G.couplingError ≤ renewalCost J D C c CF X n ∧ G.tiltError ≤ renewalCost J D C c CF X n

def EulerParentRenewalScale.activationCostSpec (CF : ℝ) (hCF : 1 ≤ CF) : EulerPacketSourceScaleChoice.CostSpec

Optional explicit extra cost for the next activation. The existing parent-square cost also controls it after multiplication by 2*CF+1.

Equations

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

theorem EulerParentRenewalScale.activationCost_eq (J : ℕ) (CF : ℝ) (hCF : 1 ≤ CF) (x : ℕ → ℝ) (n : ℕ) : (activationCostSpec CF hCF).cost J x n = (2 * CF + 1) * EulerPacketSourceScaleChoice.parentSquareRatio J x n

theorem EulerParentRenewalScale.previousShear_one_le (J : ℕ) (hJ : 1 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n : ℕ) : 1 ≤ EulerPacketSourceScaleSequence.previousShear J X n

theorem EulerParentRenewalScale.activation_ratio_le {J D : ℕ} (hJ : 1 ≤ J) {C c CF X δ : ℝ} (hCF : 1 ≤ CF) (hX : 1 ≤ X) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (e : ℝ) (he : e ≤ 1) (n : ℕ) : (CF * (1 + EulerPacketSourceScaleSequence.previousShear J X n) + e) / EulerPacketSourceScaleSequence.shear J X n ≤ (activationCostSpec CF hCF).cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n

theorem EulerParentRenewalScale.activation_smallness {J D : ℕ} (hJ : 1 ≤ J) {C c CF X δ ζ : ℝ} (hCF : 1 ≤ CF) (hX : 1 ≤ X) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (hs : EulerPacketSourceScaleChoice.SmallSeries ((activationCostSpec CF hCF).cost J (EulerPacketSourceScaleChoice.scaleSequence J X)) ζ) (e : ℝ) (he : e ≤ 1) (n : ℕ) : CF * (1 + EulerPacketSourceScaleSequence.previousShear J X n) + e ≤ ζ * EulerPacketSourceScaleSequence.shear J X n