Numerics

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Elementary numerical facts for the percolation estimates

The ABK26 percolation estimates of s.percolation.estimate are quantitative: every bound is an explicit exponential in the scale parameters. This module collects the small real-analysis facts that the quantitative modules Induction.lean and DiameterBound.lean share, so that the probabilistic arguments there are not interleaved with numerical bookkeeping.

Three groups of statements appear.

• Crude numerical bounds on log 3 and on powers of three. Only 1 ≤ log 3 and log 3 ≤ 2 are ever used, which keeps every downstream constant rational.
• Monotonicity and the tangent-line bound for the real power 3 ^ x, and the fact that two exponentials whose exponents are one unit below a common value sum to at most the exponential of that value.

References

• ABK26, s.percolation.estimate.

Elementary numerical facts

theorem Algsuperdiff.Section3.Provider.Percolation.one_le_log_three : 1 ≤ Real.log 3

theorem Algsuperdiff.Section3.Provider.Percolation.log_three_le_two : Real.log 3 ≤ 2

theorem Algsuperdiff.Section3.Provider.Percolation.succ_le_three_pow (n : ℕ) : n + 1 ≤ 3 ^ n

theorem Algsuperdiff.Section3.Provider.Percolation.one_le_three_rpow {x : ℝ} (hx : 0 ≤ x) : 1 ≤ 3 ^ x

theorem Algsuperdiff.Section3.Provider.Percolation.three_rpow_le_one {x : ℝ} (hx : x ≤ 0) : 3 ^ x ≤ 1

theorem Algsuperdiff.Section3.Provider.Percolation.one_add_le_three_rpow {x : ℝ} (hx : 0 ≤ x) : 1 + x ≤ 3 ^ x

theorem Algsuperdiff.Section3.Provider.Percolation.exp_natMul (M : ℕ) (E : ℝ) : Real.exp (↑M * E) = Real.exp E ^ M

theorem Algsuperdiff.Section3.Provider.Percolation.exp_add_exp_le {E₁ E₂ G : ℝ} (h₁ : E₁ + 1 ≤ G) (h₂ : E₂ + 1 ≤ G) : Real.exp E₁ + Real.exp E₂ ≤ Real.exp G

Two exponentials, each at least one unit below the target exponent, sum to at most the target exponential.

Passing between products and real exponentials

theorem Algsuperdiff.Section3.Provider.Percolation.exp_natMul_log_three (n : ℕ) : Real.exp (↑n * Real.log 3) = 3 ^ n

theorem Algsuperdiff.Section3.Provider.Percolation.enn_three_pow (n : ℕ) : 3 ^ n = ENNReal.ofReal (Real.exp (↑n * Real.log 3))

theorem Algsuperdiff.Section3.Provider.Percolation.enn_mul_ofReal_exp (n : ℕ) (P : ℝ) : 3 ^ n * ENNReal.ofReal (Real.exp P) = ENNReal.ofReal (Real.exp (↑n * Real.log 3 + P))

theorem Algsuperdiff.Section3.Provider.Percolation.enn_pow_ofReal_exp (M : ℕ) (E : ℝ) : ENNReal.ofReal (Real.exp E) ^ M = ENNReal.ofReal (Real.exp (↑M * E))

theorem Algsuperdiff.Section3.Provider.Percolation.enn_three_pow_mul_natCast_mul_le (n m : ℕ) (Q : ℝ) : 3 ^ n * ↑m * ENNReal.ofReal (Real.exp Q) ≤ ENNReal.ofReal (Real.exp (↑n * Real.log 3 + ↑m + Q))