The two literal initial-increment majorants are summable on the source scale sequence. The mean retains its full inverse-frequency square.

noncomputable def EulerPacketInitialScale.highMajorant (J : ℕ) (C c K : ℝ) (p q N m : ℕ) (X : ℝ) (n : ℕ) : ℝ

High majorant, given by (supportScale J X n)⁻¹^m*(frequency J X n)^m * (K*(parameterEnvelope J C c p q X n)^N)*exp (-scaleSequence J X n/8).

Equations

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

noncomputable def EulerPacketInitialScale.meanMajorant (J : ℕ) (C c K : ℝ) (p q N m : ℕ) (X : ℝ) (n : ℕ) : ℝ

Mean majorant, given by (supportScale J X n)⁻¹^m/(frequency J X n)^2 * (K*(parameterEnvelope J C c p q X n)^N).

Equations

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

theorem EulerPacketInitialScale.high_expansion (J : ℕ) (C c K : ℝ) (p q N m : ℕ) (X : ℝ) (n : ℕ) : highMajorant J C c K p q N m X n = K * C ^ N * ↑(J + n) ^ (p * N) * EulerPacketSourceScaleChoice.scaleSequence J X n ^ (q * N) * Real.exp (-(EulerPacketSourceScaleChoice.scaleSequence J X n / 8) + ↑m * (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ 2) + ↑m * (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ (7 / 2)) + ↑N * (c * (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 3)))

theorem EulerPacketInitialScale.mean_expansion (J : ℕ) (C c K : ℝ) (p q N m : ℕ) (X : ℝ) (n : ℕ) : meanMajorant J C c K p q N m X n = K * C ^ N * ↑(J + n) ^ (p * N) * EulerPacketSourceScaleChoice.scaleSequence J X n ^ (q * N) * Real.exp (-2 * (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ 2) + ↑m * (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ (7 / 2)) + ↑N * (c * (EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ 3)))

theorem EulerPacketInitialScale.current_real_power_le_previous (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 1 ≤ X) (n p : ℕ) (a : ℝ) (hpa : ↑p ≤ a) : EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J + n) ^ a ≤ EulerPacketSourceScaleChoice.scaleSequence J X n / ↑(J - 1 + n) ^ p

theorem EulerPacketInitialScale.high_summable (J : ℕ) (hJ : 2 ≤ J) (C c K : ℝ) (hC : 0 < C) (hc : 0 ≤ c) (hK : 0 < K) (p q N m : ℕ) (X : ℝ) (hX : 1 ≤ X) : Summable (highMajorant J C c K p q N m X)

theorem EulerPacketInitialScale.mean_summable (J : ℕ) (hJ : 2 ≤ J) (C c K : ℝ) (hC : 0 < C) (hK : 0 < K) (p q N m : ℕ) (X : ℝ) (hX : 1 ≤ X) : Summable (meanMajorant J C c K p q N m X)