OAI/Analysis/FourierLLogL/Thermal/Product.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Side-labeled greedy logarithmic sumset bound

  1. lemma OAI.FourierLLogL.Dyadic.Thermal.log_shift_bound line 18
  2. def OAI.FourierLLogL.Dyadic.Thermal.factorQ line 29
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.test_abs line 32
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.factor_bounds line 36
  5. def OAI.FourierLLogL.Dyadic.Thermal.Qp line 54
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.q_exp_constant line 57
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.q_step line 61
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.span_collection line 83
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.conditional_if_ex line 105
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.append_cost line 112
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.cheap_span line 134
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.sumset_est line 162