OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/LogarithmName.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A terminating rational search for the logarithm of a positive named real. The search compares certified exponential balls with the input name; it never uses a test of equality or ordering on real numbers.

  1. def OAI.ForcedComputation.logSearchData line 15
  2. def OAI.ForcedComputation.logReady line 18
  3. instance OAI.ForcedComputation.(instance at line 26) line 26
  4. theorem OAI.ForcedComputation.errorTolerance_tendsto line 31
  5. theorem OAI.ForcedComputation.fastRealName_tendsto line 37
  6. theorem OAI.ForcedComputation.logReady_exists line 44
  7. def OAI.ForcedComputation.logApprox line 76

    Source documentation

    Rational bisection is not required: an exhaustive finite search of strict certified brackets terminates for every positive input.

    def logApprox {x : ℝ} (a : ℕ → ℚ) (hx : 0 < x) (ha : IsFastRealName a x)
    (ε : ℚ) (hε : 0 < ε) : ℚ :=
…
  8. theorem OAI.ForcedComputation.logApprox_spec line 83
  9. def OAI.ForcedComputation.logFastName line 119
  10. theorem OAI.ForcedComputation.logFastName_spec line 122