OAI/Analysis/Steinitz/Adaptive.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Energy-preserving sections and adaptive coordinate selection.

  1. lemma OAI.ShiftedSections.section_crossing line 15
  2. lemma OAI.ShiftedSections.symbol_mul line 23
  3. lemma OAI.ShiftedSections.section_rate_le line 33
  4. lemma OAI.ShiftedSections.section_bound_positive line 78
  5. lemma OAI.ShiftedSections.section_bound line 92
  6. abbrev OAI.ShiftedSections.Coeff line 135
  7. structure OAI.ShiftedSections.Good line 137
  8. lemma OAI.ShiftedSections.Good.zero_mem line 146
  9. lemma OAI.ShiftedSections.Good.section line 149
  10. def OAI.ShiftedSections.backward line 157
  11. lemma OAI.ShiftedSections.backward_good line 161
  12. def OAI.ShiftedSections.walk line 167
  13. lemma OAI.ShiftedSections.exists_walk line 173
  14. lemma OAI.ShiftedSections.adaptive_signs line 190