OAI/Analysis/FourierLLogL/Paths/Ticket.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The uniform output path

  1. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.entry line 19
  2. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.entry_share line 21
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.old_budget line 24
  4. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scaleC line 51
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scale_one line 52
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scale_pos line 53
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.scale_side line 54
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.prescale line 56
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.marker_one line 63
  10. def OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.broadMass line 76
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Paths.Troupe.prelude line 79