OAI/Analysis/LipschitzHilbert/Trees/SourceParameters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual rounded dyadic parameters in the manuscript.

  1. def OAI.LipschitzHilbert.SourceParameters.blockCount line 17
  2. def OAI.LipschitzHilbert.SourceParameters.stepExponent line 19
  3. def OAI.LipschitzHilbert.SourceParameters.step line 21
  4. def OAI.LipschitzHilbert.SourceParameters.branching line 23
  5. def OAI.LipschitzHilbert.SourceParameters.branchingNat line 25
  6. theorem OAI.LipschitzHilbert.SourceParameters.branchingNat_cast line 27
  7. theorem OAI.LipschitzHilbert.SourceParameters.step_pos line 30
  8. theorem OAI.LipschitzHilbert.SourceParameters.branching_pos line 32
  9. theorem OAI.LipschitzHilbert.SourceParameters.log_step_bounds line 34
  10. theorem OAI.LipschitzHilbert.SourceParameters.log_branching_le line 55
  11. theorem OAI.LipschitzHilbert.SourceParameters.eventually_branching_separation line 66

    Source documentation

    The actual rounded dyadic branching satisfies the scale separation B^100 ≤ exp(L^0.9) eventually, with no real-valued stand-in for B.

    theorem eventually_branching_separation :
    ∀ᶠ L : ℝ in atTop, branching L ^ 100 ≤ Real.exp (L ^ (9 / 10 : ℝ)) := by
…

    Mentions: OAI.LipschitzHilbert.SourceParameters.branching