Potential Bounds

Bounds for the harmonic potential

theorem FD1D.harmonicPotential_nonneg {a : ℝ} (ha : 0 < a) (k : ℕ) : 0 ≤ harmonicPotential a k

The node potential is nonnegative when the regularization is positive.

theorem FD1D.harmonicPotential_le_log_one_add {a : ℝ} (ha : 0 < a) (k : ℕ) : harmonicPotential a k ≤ Real.log (1 + ↑k / a)

The shifted harmonic sum is bounded by its integral: sum_{j=1}^k 1 / (a+j) ≤ log (1+k/a).

Global potential bounds

theorem FD1D.globalHarmonicPotential_nonneg {L : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} (ha : 0 < a) : 0 ≤ globalHarmonicPotential L a N

Every global harmonic potential is nonnegative.

theorem FD1D.globalHarmonicPotential_le_log_one_add {L m : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} (ha : 0 < a) (hN : ∀ (d : ℕ) (v : DyadicNode d), N d v ≤ m) : globalHarmonicPotential L a N ≤ Real.log (1 + ↑m / a)

If all node counts are at most m, then the global potential is at most log (1 + m/a).

theorem FD1D.globalHarmonicPotential_bounds {L m : ℕ} {a : ℝ} {N : (d : ℕ) → DyadicNode d → ℕ} (ha : 0 < a) (hN : ∀ (d : ℕ) (v : DyadicNode d), N d v ≤ m) : 0 ≤ globalHarmonicPotential L a N ∧ globalHarmonicPotential L a N ≤ Real.log (1 + ↑m / a)

The two-sided global potential estimate used in the transient argument.

The logarithmic budget for the chosen parameter

theorem FD1D.two_hundred_mul_log_one_add_le_parameterA {m : ℕ} (hm : 1 ≤ m) : 200 * Real.log (1 + ↑m / ↑(parameterA m)) ≤ ↑(parameterA m)

The chosen parameter dominates 200 * log (1 + m/a).

theorem FD1D.two_hundred_mul_log_one_add_div_parameterA_le_one {m : ℕ} (hm : 1 ≤ m) : 200 * Real.log (1 + ↑m / ↑(parameterA m)) / ↑(parameterA m) ≤ 1

Divided form of the logarithmic budget appearing in Section 5.

Finite Jensen helper

theorem FD1D.finite_average_sqrt_le_sqrt_average {T : ℕ} (hT : 0 < T) (f : ℕ → ℝ) (hf : ∀ t < T, 0 ≤ f t) : (∑ t ∈ Finset.range T, √(f t)) / ↑T ≤ √((∑ t ∈ Finset.range T, f t) / ↑T)

Jensen's inequality for the square root of a nonnegative finite average.