Abstract real lemmas for the no-selection limit argument

• the two-diffusivity coefficient |a-b|/(2√(ab)) is controlled by |log(a/b)|;
• closeness of two logarithms to the same value;
• interpolation min(A, H h^μ) ≤ √(AH) h^{μ/2}.

theorem AVenhance.Infra.FullTheorem.diffusivity_ratio_le {a b d : ℝ} (ha : 0 < a) (hb : 0 < b) (hd : |Real.log (a / b)| ≤ d) (hd1 : d ≤ 1) : |a - b| / (2 * √(a * b)) ≤ 2 * d

|a-b|/(2√(ab)) ≤ 2 |log (a/b)| when |log (a/b)| ≤ 1.

theorem AVenhance.Infra.FullTheorem.log_ratio_le {a b D s e₁ e₂ : ℝ} (ha : 0 < a) (hb : 0 < b) (hD : 0 < D) (h1 : |Real.log (a / D) - s| ≤ e₁) (h2 : |Real.log (b / D) - s| ≤ e₂) : |Real.log (a / b)| ≤ e₁ + e₂

Two logarithms close to the same number s: the ratio has small logarithm.

theorem AVenhance.Infra.FullTheorem.min_interp {x A H h μ : ℝ} (hh : 0 ≤ h) (hx0 : 0 ≤ x) (h1 : x ≤ A) (h2 : x ≤ H * h ^ μ) : x ≤ √(A * H) * h ^ (μ / 2)

min(A, H h^μ) ≤ √(A H) h^{μ/2}.