OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarScaleChoice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single fixed polynomial exponent gives uniform hopping brackets for every input size. Exponential domination selects that exponent once.

  1. theorem OAI.ContinuumCoulomb.exists_planar_scale_conditions_above line 13
  2. theorem OAI.ContinuumCoulomb.exists_planar_scale_conditions line 64
  3. theorem OAI.ContinuumCoulomb.exists_planar_polynomial_brackets_above line 76

    Source documentation

    For every polynomial target range, a fixed power λ=N^k brackets that range uniformly at the two allowed contact lengths, for all real N≥2.

    theorem exists_planar_polynomial_brackets_above (B : ℝ) (A : ℕ) {ε : ℝ} (hε : 0 < ε) (hε₁ : ε < 1) :
    ∃ k : ℕ, 0 < k ∧ B ≤ (k : ℝ) ∧ ∀ N : ℝ, 2 ≤ N →
      2 ≤ (1 - ε) * ((k : ℝ) * Real.log N) ∧
      N ^ A ≤ N ^ k * planarHopping ((1 - ε) * ((k : ℝ) * Real.log N)) ∧
      N ^ k * planarHopping ((1 + ε) * ((k : ℝ) * Real.log N)) ≤ (N ^ A)⁻¹ := by
…

    Mentions: OAI.ContinuumCoulomb.planarHopping

  4. theorem OAI.ContinuumCoulomb.exists_planar_polynomial_brackets line 94