OAI/Analysis/FourierLLogL/Capture/Flex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Entropy relative to the adaptive product

  1. abbrev OAI.FourierLLogL.Dyadic.Procedure.Capture.ProductRef line 14
  2. def OAI.FourierLLogL.Dyadic.Procedure.Capture.normQ line 15
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.normQ_pos line 18
  4. def OAI.FourierLLogL.Dyadic.Procedure.Capture.flex line 24
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.flex_nonneg line 28
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.flex_one line 60
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.track_shift line 65
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.flex_keep line 75
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.flex_down line 116