Convergence estimates for the actual quadratic scale recurrence in (37). The sequence is reindexed so that x 0 = x_{J-1} and x (n+1) = (J+n)^2 x n; hence J+n is the stage index in the source.

theorem EulerScale.quadratic_growth_pos (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (n : ℕ) : 0 < x n

Positivity propagates through the scale recurrence from any positive initial scale.

theorem EulerScale.stage_inv_tendsto_zero (J : ℕ) : Filter.Tendsto (fun (n : ℕ) => (↑(J + n))⁻¹) Filter.atTop (nhds 0)

The reciprocal of the stage index tends to zero.

theorem EulerScale.polynomial_over_growth_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A : ℕ) : Summable fun (n : ℕ) => ↑(J + n) ^ A / x n

Every fixed polynomial in the stage index divided by the scale is summable.

theorem EulerScale.exp_neg_le_reciprocal (t : ℝ) (ht : 0 < t) : Real.exp (-t) ≤ 1 / t

A simple exponential majorization requiring no numerical approximations.

theorem EulerScale.exponential_decay_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A : ℕ) (b : ℝ) (hb : 0 < b) : Summable fun (n : ℕ) => Real.exp (-b * (x n / ↑(J + n) ^ A))

Every exponential decay in a scale divided by a fixed natural power is summable.

theorem EulerScale.exponential_decay_real_power_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A b : ℝ) (hb : 0 < b) : Summable fun (n : ℕ) => Real.exp (-b * (x n / ↑(J + n) ^ A))

The same decay conclusion holds for every real power, including 7/2.

theorem EulerScale.abs_log_growth_le (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (n : ℕ) : |Real.log (x n)| ≤ (|Real.log (x 0)| + 2) * ↑(J + n) ^ 2

The logarithm of the rapidly growing scale still has a quadratic polynomial bound.

theorem EulerScale.polynomial_log_over_growth_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A : ℕ) : Summable fun (n : ℕ) => ↑(J + n) ^ A * |Real.log (x n)| / x n

Every polynomial weight times |log x|/x is summable.

theorem EulerScale.polynomial_log_over_growth_tendsto_zero (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(J + n) ^ A * Real.log (x n) / x n) Filter.atTop (nhds 0)

The logarithmic term on the right side of (39) tends to zero with every fixed polynomial weight.

theorem EulerScale.polynomial_stage_log_over_growth_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A : ℕ) : Summable fun (n : ℕ) => ↑(J + n) ^ A * Real.log ↑(J + n) / x n

The logarithm of the stage index is also harmless in every polynomially weighted scale sum.

theorem EulerScale.stage_sq_div_real_power_tendsto_zero (J : ℕ) (hJ : 1 ≤ J) (A : ℝ) (hA : 3 ≤ A) : Filter.Tendsto (fun (n : ℕ) => ↑(J + n) ^ 2 / ↑(J + n) ^ A) Filter.atTop (nhds 0)

A power at least three in the denominator dominates the square from 1/log k_j.

theorem EulerScale.stage_sq_div_predecessor_power_tendsto_zero (J : ℕ) (hJ : 2 ≤ J) (A : ℕ) (hA : 3 ≤ A) : Filter.Tendsto (fun (n : ℕ) => ↑(J + n) ^ 2 / ↑(J - 1 + n) ^ A) Filter.atTop (nhds 0)

The previous-stage frequency and shear terms have vanishing relative logarithms.

theorem EulerScale.log_sum_exp_bounds {ι : Type u_1} [Fintype ι] [Nonempty ι] (a : ι → ℝ) (ha : ∀ (i : ι), 0 ≤ a i) : 0 ≤ Real.log (∑ i : ι, Real.exp (a i)) ∧ Real.log (∑ i : ι, Real.exp (a i)) ≤ Real.log ↑(Fintype.card ι) + ∑ i : ι, a i

A finite sum of positive exponential scales has an explicit logarithmic upper bound.

theorem EulerScale.log_sum_exp_mul_tendsto_zero {ι : Type u_1} [Fintype ι] [Nonempty ι] (a : ι → ℕ → ℝ) (r : ℕ → ℝ) (ha : ∀ (i : ι) (n : ℕ), 0 ≤ a i n) (hr : ∀ (n : ℕ), 0 ≤ r n) (hrlim : Filter.Tendsto r Filter.atTop (nhds 0)) (halim : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => a i n * r n) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => Real.log (∑ i : ι, Real.exp (a i n)) * r n) Filter.atTop (nhds 0)

Finite aggregation preserves a logarithmic scale separation proved for each explicit term.

theorem EulerScale.quadratic_growth_one_le (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (n : ℕ) : 1 ≤ x n

A starting scale at least one stays at least one.

noncomputable def EulerScale.sourceParameterExponent (J : ℕ) (Cbase Cstar : ℝ) (x : ℕ → ℝ) (i : Fin 8) (n : ℕ) : ℝ

The logarithms of the eight terms in the source's aggregate parameter: the fixed base constant; the previous frequency power; inverse support and spike scales; the present and previous shears; and the present and previous geometric sizes.

Equations

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

noncomputable def EulerScale.sourceParameterAggregate (J : ℕ) (Cbase Cstar : ℝ) (x : ℕ → ℝ) (n : ℕ) : ℝ

The sum of precisely those eight positive parameter terms.

Equations

• EulerScale.sourceParameterAggregate J Cbase Cstar x n = ∑ i : Fin 8, Real.exp (EulerScale.sourceParameterExponent J Cbase Cstar x i n)

theorem EulerScale.sourceParameterExponent_nonneg (J : ℕ) (hJ : 2 ≤ J) (Cbase Cstar : ℝ) (hCbase : 1 ≤ Cbase) (hCstar : 0 ≤ Cstar) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (i : Fin 8) (n : ℕ) : 0 ≤ sourceParameterExponent J Cbase Cstar x i n

theorem EulerScale.sourceParameterExponent_relative_tendsto_zero (J : ℕ) (hJ : 2 ≤ J) (Cbase Cstar : ℝ) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (i : Fin 8) : Filter.Tendsto (fun (n : ℕ) => sourceParameterExponent J Cbase Cstar x i n * (↑(J + n) ^ 2 / x n)) Filter.atTop (nhds 0)

Every explicitly defined parameter term is negligible on the logarithmic frequency scale.

theorem EulerScale.sourceParameterAggregate_eq (J : ℕ) (hJ : 1 ≤ J) (Cbase Cstar : ℝ) (hCbase : 0 < Cbase) (x : ℕ → ℝ) (hxp : ∀ (n : ℕ), 0 < x n) (n : ℕ) : sourceParameterAggregate J Cbase Cstar x n = Cbase + Real.exp (Cstar * x n / ↑(J - 1 + n) ^ 4) + Real.exp (x n / ↑(J + n) ^ (7 / 2)) + Real.exp (x n / ↑(J + n) ^ 3) + Real.exp (x n / ↑(J + n) ^ 5) + Real.exp (x n / ↑(J - 1 + n) ^ 7) + ↑(J + n) ^ 2 * x n + x n

Expansion of the aggregate into the scales listed immediately before (39).

theorem EulerScale.source_parameters_separated (J : ℕ) (hJ : 2 ≤ J) (Cbase Cstar : ℝ) (hCbase : 1 ≤ Cbase) (hCstar : 0 ≤ Cstar) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) : Filter.Tendsto (fun (n : ℕ) => Real.log (sourceParameterAggregate J Cbase Cstar x n) / (x n / ↑(J + n) ^ 2)) Filter.atTop (nhds 0)

The full logarithmic separation in (39), for the explicit aggregate of all eight scales. Its hypotheses contain only the scale recurrence and fixed positivity conditions; the logarithmic separation is a conclusion.

theorem EulerScale.perturbed_exponential_decay_summable (J : ℕ) (hJ : 1 ≤ J) (x : ℕ → ℝ) (hx0 : 0 < x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (A b : ℝ) (hb : 0 < b) (e : ℕ → ℝ) (he : Filter.Tendsto (fun (n : ℕ) => e n / (x n / ↑(J + n) ^ A)) Filter.atTop (nhds 0)) : Summable fun (n : ℕ) => Real.exp (-b * (x n / ↑(J + n) ^ A) + e n)

Exponential scale decay remains summable after a quantitatively vanishing relative error.

theorem EulerScale.initial_increment_majorants_summable (J : ℕ) (hJ : 2 ≤ J) (Cbase Cstar : ℝ) (hCbase : 1 ≤ Cbase) (hCstar : 0 ≤ Cstar) (x : ℕ → ℝ) (hx0 : 1 ≤ x 0) (hx : ∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) (m C b : ℝ) (hb : 0 < b) : (Summable fun (n : ℕ) => Real.exp (-b * x n + m * (x n / ↑(J + n) ^ 2) + m * (x n / ↑(J + n) ^ (7 / 2)) + C * Real.log (sourceParameterAggregate J Cbase Cstar x n))) ∧ Summable fun (n : ℕ) => Real.exp (-2 * (x n / ↑(J + n) ^ 2) + m * (x n / ↑(J + n) ^ (7 / 2)) + C * Real.log (sourceParameterAggregate J Cbase Cstar x n))

Both initial-increment exponential bounds after (22) are summable. In particular, the mean estimate needs no extra power of the oscillation frequency.