OAI/Combinatorics/EditApproximation/Geometry/ParameterLocalAsymptotics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Scalar bounds for the local enumeration exponent.

  1. theorem OAI.EditApproximation.inputHeight_real_tendsto line 12
  2. theorem OAI.EditApproximation.smallLog_polynomial_div_height_tendsto line 19

    Source documentation

    Every fixed polynomial in the computed small logarithm is negligible relative to the computed height.

    theorem smallLog_polynomial_div_height_tendsto (k : ℕ) :
    Tendsto (fun N => (inputSmallLog N : ℝ) ^ k / inputHeight N) atTop (𝓝 0) := by
…

    Mentions: OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight

  3. theorem OAI.EditApproximation.computed_branching_square_le_height line 35
  4. theorem OAI.EditApproximation.branching_smallLog_polynomial_div_height_tendsto line 43

    Source documentation

    This directly controls the scalar exponent M q ell occurring in the local wide-action enumeration.

    theorem branching_smallLog_polynomial_div_height_tendsto (k : ℕ) :
    Tendsto (fun N => ((integerParameters N).M : ℝ) *
      (inputSmallLog N : ℝ) ^ k / inputHeight N) atTop (𝓝 0) := by
…

    Mentions: OAI.EditApproximation.integerParameters, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight

  5. theorem OAI.EditApproximation.coarseExponent_le_smallLog line 68
  6. theorem OAI.EditApproximation.local_enumeration_exponent_div_height_tendsto line 75
  7. theorem OAI.EditApproximation.inputHeight_real_log line 95
  8. theorem OAI.EditApproximation.encoding_exponent_div_height_tendsto line 99
  9. theorem OAI.EditApproximation.height_log_sandwich line 123