OAI/Analysis/FourierLLogL/Snapshot/Measure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Snapshot.RingN line 15
  2. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.shade line 16
  3. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.shine line 18
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.shade_close line 21
  5. abbrev OAI.FourierLLogL.Dyadic.Procedure.Snapshot.TileN line 45
  6. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.tiles line 47
  7. abbrev OAI.FourierLLogL.Dyadic.Procedure.Snapshot.Dome line 50
  8. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.sight line 52
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.see_as_H line 56
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Snapshot.sight_budget line 69
  11. def OAI.FourierLLogL.Dyadic.Procedure.Snapshot.switch line 103
  12. theorem OAI.FourierLLogL.Dyadic.Procedure.Snapshot.painted line 105