OAI/Analysis/HardSphere/Cutoffs/ChordLift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicCutoff.chordLift line 18
  2. lemma OAI.PeriodicCutoff.chordLift_periodic line 20
  3. def OAI.PeriodicCutoff.chord line 28
  4. lemma OAI.PeriodicCutoff.chord_coe line 30
  5. lemma OAI.PeriodicCutoff.chordLift_smooth line 34
  6. lemma OAI.PeriodicCutoff.chord_continuous line 38
  7. lemma OAI.PeriodicCutoff.chordLift_derivative line 42
  8. lemma OAI.PeriodicCutoff.chordLift_derivative_sq_le line 49
  9. lemma OAI.PeriodicCutoff.centered_representative line 59
  10. lemma OAI.PeriodicCutoff.chord_nonneg line 73
  11. lemma OAI.PeriodicCutoff.chord_le_norm_sq line 77
  12. lemma OAI.PeriodicCutoff.norm_sq_le_chord line 93