NormalizedLevelAlgebra.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Normalization algebra for the harmonic level recurrence

theorem OAI.RegularPointCoordinates.normalized_level_identity line 11

Source documentation

Scaling the level energy by the outer volume removes that volume from the superlinear recurrence.

theorem normalized_level_identity {V J C d a b α : ℝ}
    (hV : 0 < V) (hJ : 0 ≤ J) (ha : 0 < a) (hb : 0 < b) (hα : 0 < α) (i : ℕ) :
    (C*V^(-α)*(d*b^i)*J*(a*b^i*J)^α)/V =
      (C*d*a^α)*(b^(1+α))^i*(J/V)^(1+α) := by
…

theorem OAI.RegularPointCoordinates.dyadic_inner_radii line 27

Source documentation

The dyadic radii stay between one half and three quarters of R.

theorem dyadic_inner_radii {R : ℝ} (hR : 0 < R) (i : ℕ) :
    0 ≤ R/2+R/(4*2^(i+1)) ∧
    R/2+R/(4*2^(i+1)) < R/2+R/(4*2^i) ∧
    R/2+R/(4*2^i) < R := by
…

theorem OAI.RegularPointCoordinates.dyadic_level_gap_bounds line 46

Source documentation

The reciprocal squared level gap and the cutoff energy grow by four.

theorem dyadic_level_gap_bounds {R : ℝ} (hR : 0 < R) (i : ℕ) :
    0 ≤ 1-(2^i:ℝ)⁻¹ ∧
    1-(2^i:ℝ)⁻¹ < 1-(2^(i+1):ℝ)⁻¹ ∧
    ((1-(2^(i+1):ℝ)⁻¹)-(1-(2^i:ℝ)⁻¹))⁻¹^2 = 4*4^i ∧
    10*R^2*(((R/2+R/(4*2^i))-(R/2+R/(4*2^(i+1))))⁻¹)^2+1 ≤ 641*4^i := by
…