The literal source truncation floor(k^ϑ), ϑ=10⁻⁶, meets the packet and correction guards from finitely many fixed-cost bounds.

noncomputable def EulerPacketSourceFrequency.theta : ℝ

Theta, given by 1/1000000.

Equations

• EulerPacketSourceFrequency.theta = 1 / 1000000

noncomputable def EulerPacketSourceFrequency.expansion (k : ℝ) : ℝ

Expansion, given by k^theta.

Equations

• EulerPacketSourceFrequency.expansion k = k ^ EulerPacketSourceFrequency.theta

noncomputable def EulerPacketSourceFrequency.truncation (k : ℝ) : ℕ

Truncation, given by Nat.floor (expansion k).

Equations

• EulerPacketSourceFrequency.truncation k = ⌊EulerPacketSourceFrequency.expansion k⌋₊

noncomputable def EulerPacketSourceFrequency.smallPower (k : ℝ) : ℝ

Small power, given by k^(theta/100).

Equations

• EulerPacketSourceFrequency.smallPower k = k ^ (EulerPacketSourceFrequency.theta / 100)

theorem EulerPacketSourceFrequency.expansion_pos (k : ℝ) (hk : 0 < k) : 0 < expansion k

theorem EulerPacketSourceFrequency.truncation_bounds (k : ℝ) (hk : 1 ≤ k) : 1 ≤ truncation k ∧ expansion k - 1 ≤ ↑(truncation k) ∧ ↑(truncation k) ≤ expansion k

theorem EulerPacketSourceFrequency.smallPower_le_expansion (k : ℝ) (hk : 1 ≤ k) : smallPower k ≤ expansion k

theorem EulerPacketSourceFrequency.smallPower_le_frequency (k : ℝ) (hk : 1 ≤ k) : smallPower k ≤ k

theorem EulerPacketSourceFrequency.smallPower_le_gradeCap (k : ℝ) (hk : 1 ≤ k) : smallPower k ≤ k ^ (1 / 100)

theorem EulerPacketSourceFrequency.tailBase_frequency (R H C k : ℝ) (hC : 0 ≤ C) (hk : 1 ≤ k) (hc : EulerPacketCoarseMajorant.tailPolynomialConstant R H C ≤ smallPower k) : EulerPacketCoarseMajorant.tailBase R H C (truncation k) ≤ k ^ (1 / 100)

theorem EulerPacketSourceFrequency.smallPower_le_exp_sqrt (k : ℝ) (hk : 0 < k) : smallPower k ≤ Real.exp √(expansion k)

The source's very small power is below the exponential margin in the error target exp(-sqrt(k^ϑ)).

theorem EulerPacketSourceFrequency.correction_guards (C T D ρ0 k : ℝ) (hk : 1 ≤ k) (hρ : 0 < ρ0) (hX : 64 ≤ expansion k) (hlog : 1 ≤ Real.log k) (hgrowth : 12 * C * T ≤ smallPower k) (hdrift : 8 * C * T * D / ρ0 ≤ smallPower k) (herror : 8 * C * T / ρ0 ≤ smallPower k) : 2 * EulerPacketCorrectionScalar.residual k (expansion k) * Real.exp (3 * C * T) ≤ EulerPacketCorrectionScalar.delta (expansion k) / 2 ∧ 2 * C * (D / k + EulerPacketCorrectionScalar.delta (expansion k)) * T ≤ ρ0 / 2

theorem EulerPacketSourceFrequency.fixed_costs_eventually (cost : Finset ℝ) : ∀ᶠ (k : ℝ) in Filter.atTop, 4 ≤ k ∧ 64 ≤ expansion k ∧ 1 ≤ Real.log k ∧ ∀ c ∈ cost, c ≤ smallPower k

Every finite list of fixed source costs fits the required very small power after one sufficiently large frequency choice.