OAI/Analysis/FourierLLogL/Capture/MaskKernel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Band-limited cutoffs

  1. def OAI.FourierLLogL.Dyadic.Procedure.Capture.limit line 14
  2. def OAI.FourierLLogL.Dyadic.Procedure.Capture.limitR line 15
  3. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.limit_mul line 17
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.limit_scale line 26
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.limit_const line 28
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.limit_pow line 32
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.limit_star line 39
  8. def OAI.FourierLLogL.Dyadic.Procedure.Capture.tile line 49

    Source documentation

    Dirichlet factor normalized to one.

    private def tile (M d : ℕ) (x : Grid M) := (d:ℂ)⁻¹ * ∑ i∈Finset.range d, chi (i:Grid M) x

    Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.chi

  9. def OAI.FourierLLogL.Dyadic.Procedure.Capture.slab line 50
  10. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tile_limit line 52
  11. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.slab_limit line 62
  12. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.slab_nonneg line 69
  13. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.slab_total line 71
  14. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tile_lower line 100
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.tile_upper line 130
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Capture.boosted line 155