OAI/Analysis/FourierLLogL/Thermal/Packing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Gap of a metric ball

  1. def OAI.FourierLLogL.Dyadic.Thermal.gap line 16
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.ball_pos line 18
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.gap_zero line 21
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.half_q_ball line 39
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.gap_lower line 48
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.overlap_bound line 63
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_diff line 96
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.rad_diff line 101
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.log_pair line 107
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.gap_packing line 172