OAI/Analysis/FourierLLogL/Thermal/Spatial.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The spatial form and the discrete Gaussian bounds

  1. lemma OAI.FourierLLogL.Dyadic.Thermal.wave_at_one line 15
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.wave_at_diam line 22
  3. theorem OAI.FourierLLogL.Dyadic.Thermal.cost_diam line 29
  4. def OAI.FourierLLogL.Dyadic.Thermal.S line 51

    Source documentation

    Spatial form, specified by inverse width

    def S (M : ℕ) (R : ℝ) : Form M := fun s => if s=1 then R^2 else 0

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form

  5. lemma OAI.FourierLLogL.Dyadic.Thermal.S_nonneg line 53
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.form_S line 58
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.scale_S line 60
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.S_mono line 65
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.expU_ray line 69
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.q_S_upper line 101
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.q_S_lower line 129
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.q_S_upper' line 168
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.F_S_lower line 174
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.F_S_upper line 181
  15. lemma OAI.FourierLLogL.Dyadic.Thermal.S_energy line 189
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.S_cost line 208
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.S_variance line 214
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_S line 219
  19. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_short line 234
  20. lemma OAI.FourierLLogL.Dyadic.Thermal.q_short line 244