OAI/MathematicalPhysics/Transonic/Exterior/Range.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.FixedInterval.intersect line 9
  2. lemma OAI.SepticProfile.FixedInterval.holds_intersect line 14
  3. lemma OAI.SepticProfile.FixedInterval.holds_of_bound line 33
  4. lemma OAI.SepticProfile.FixedInterval.holds_root line 38
  5. lemma OAI.SepticProfile.FixedInterval.powers_enclosed line 71
  6. lemma OAI.SepticProfile.FixedInterval.normalized_monomials line 82
  7. def OAI.SepticProfile.FixedInterval.hornerBox line 112

    Source documentation

    Backward Horner recurrence; after n steps this is evaluation of the suffix.

    def hornerBox (Q : ℤ) (a : ℕ → Box) (x : Box) (lo : ℕ) : ℕ → Box
  | 0 => zero
  | n+1 => add (a lo) (mul Q x (hornerBox Q a x (lo+1) n))

    Mentions: OAI.SepticProfile.FixedInterval.Box, OAI.SepticProfile.FixedInterval.zero, OAI.SepticProfile.FixedInterval.add, OAI.SepticProfile.FixedInterval.mul

  8. def OAI.SepticProfile.FixedInterval.hornerValue line 116
  9. lemma OAI.SepticProfile.FixedInterval.holds_horner line 120
  10. lemma OAI.SepticProfile.FixedInterval.hornerValue_sum line 130