OAI/Analysis/FourierLLogL/Capture/Book.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FourierLLogL.Dyadic.Procedure.Capture.atReach line 15
  2. def OAI.FourierLLogL.Dyadic.Procedure.Capture.tinted line 18
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.atReach_neg line 21
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tinted_mul line 26
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tinted_cancel line 40
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tinted_one line 52
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tinted_extend line 58
  8. structure OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart line 92
  9. def OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart.classic line 98
  10. def OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart.size line 99
  11. structure OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart.Sound line 100
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart.classic_sound line 105
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.Chart.Sound.pos line 107