Every higher wall power absorbs a logarithmic quadratic loss

Proved

BianchiIX.exists_rpow_log_quadratic_scale

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

For every real $p>2$ there exists $a_*>0$ such that

0<a\leq a_*\quad\Longrightarrow\quad a\leq1,\quad a^p\leq a^2,\quad a^p(1+|\log a|)\leq a^2.

Preamble

import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

namespace BianchiIX
end BianchiIX

noncomputable section
open BianchiIX
open Set Filter
open scoped Topology

Formal statement

theorem BianchiIX.exists_rpow_log_quadratic_scale {p : ℝ} (hp : 2 < p) :
    ∃ astar > (0 : ℝ), ∀ a ∈ Ioc (0 : ℝ) astar,
      a ≤ 1 ∧ a ^ p ≤ a ^ 2 ∧ a ^ p * (1 + |Real.log a|) ≤ a ^ 2 := by sorry

Source

https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Analysis/ShearTailEndpointScale.lean#L10-L40

View graph