OAI/Analysis/PathSelection/SecondClockFields.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Second-clock multiplication, differentiation and transported sector fields.

  1. lemma OAI.DegeneratingTrees.Clock.ClockGerm.finset_sum line 15
  2. theorem OAI.DegeneratingTrees.Clock.ClockGerm.mul line 25
  3. lemma OAI.DegeneratingTrees.Clock.ValidClocks.second_lowerData line 55
  4. theorem OAI.DegeneratingTrees.Clock.ClockGerm.second_inv line 99
  5. lemma OAI.DegeneratingTrees.Clock.transported_first_deriv_mem line 119
  6. lemma OAI.DegeneratingTrees.Clock.ValidClocks.second_differentialData line 147
  7. lemma OAI.DegeneratingTrees.Clock.ClockGerm.second_of_lower line 209
  8. lemma OAI.DegeneratingTrees.Clock.ExpansionOver.deriv_mem line 217
  9. theorem OAI.DegeneratingTrees.Clock.ClockGerm.second_deriv line 226
  10. def OAI.DegeneratingTrees.Clock.TransportedField line 261
  11. lemma OAI.DegeneratingTrees.Clock.transported_lowerSectorData line 264
  12. lemma OAI.DegeneratingTrees.Clock.transported_deriv_mem line 294
  13. lemma OAI.DegeneratingTrees.Clock.tendsto_star_sectorInfinity line 323
  14. lemma OAI.DegeneratingTrees.Clock.SectorInverse.reflection_eq line 329
  15. lemma OAI.DegeneratingTrees.Clock.transported_conj_mem line 338
  16. lemma OAI.DegeneratingTrees.Clock.SectorSlow.log_inverse line 363
  17. lemma OAI.DegeneratingTrees.Clock.SectorInverse.log_small line 384