Uniform local C2 scales. The ambient scale and the local scale stay distinct.

noncomputable def G12LocalScale.nu (x T : ℝ) : ℝ

Equations

• G12LocalScale.nu x T = Real.log T / Real.log x

noncomputable def G12LocalScale.level (x T ζ : ℝ) : ℝ

Equations

• G12LocalScale.level x T ζ = x ^ ((5 - 5 * G12LocalScale.nu x T) / 9 - ζ)

theorem G12LocalScale.log_level {x T ζ : ℝ} (hx : 1 < x) : Real.log (level x T ζ) = (5 / 9 - ζ) * Real.log x - 5 / 9 * Real.log T

theorem G12LocalScale.recover_T {x T : ℝ} (hx : 1 < x) (hT : 0 < T) : x ^ nu x T = T

theorem G12LocalScale.logarithmic_geometry {L X Y ζ : ℝ} (hL : 0 < L) (hz : 0 < ζ) (hzsmall : ζ ≤ 1 / 100) (hXlo : (1 - ζ / 4) * L ≤ X) (hXhi : X ≤ (1 + ζ / 4) * L) (hYlo : (4 / 53 - ζ / 4) * L ≤ Y) (hYhi : Y ≤ 1 / 10 * L) : 0 < X ∧ ζ ≤ Y / X ∧ Y / X ≤ 1 / 10 + ζ / 10 ∧ L / 3 ≤ (5 / 9 - ζ) * X - 5 / 9 * Y ∧ (5 / 9 - ζ) * X - 5 / 9 * Y ≤ L

Pure algebraic distortion estimate, separated from the uniform cutoff.

theorem G12LocalScale.reciprocal_bridge {a b ζ δ : ℝ} (ha : 1 / 2 ≤ a) (hb : 1 / 3 ≤ b) (hab : a - 2 * ζ ≤ b) (hδ : 0 ≤ δ) (hsmall : 48 * ζ ≤ δ) : 4 / b ≤ 4 / a + δ

The reciprocal distortion costs at most 48 * ζ, uniformly in the endpoint.