OAI/Analysis/FourierLLogL/Assembly/Rail.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.blend line 18
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.subtC line 23
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.subtR line 28
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.subt_constant line 33
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.subt_neg line 38
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.subt_norm line 43
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.trip_attend line 49
  8. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.spaceRent line 66
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.length_fee line 67
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.aired line 78
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.rail_fee line 81
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.straight_fee line 114
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.decode_track line 126
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.below_decode line 147