PlanarUniformCalibration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform contact calibration with a single fixed polynomial scale.

theorem OAI.ContinuumCoulomb.exists_uniform_planar_calibration_above line 14

Source documentation

Every continuous distance-dependent target in a polynomial range is attained by the actual amplified contact hopping at a permitted length. The same fixed polynomial exponent works for every input size and every target in that range.

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

Mentions: OAI.ContinuumCoulomb.planarHopping

theorem OAI.ContinuumCoulomb.exists_uniform_planar_calibration line 46