OAI/Analysis/FourierLLogL/Thermal/Positive.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Positive Fourier expansions

  1. def OAI.FourierLLogL.Dyadic.Thermal.ac line 15
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.ac_mul line 16
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.ac_scale line 24
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.ac_sum line 29
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.ac_const line 33
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.ac_wave line 40
  7. def OAI.FourierLLogL.Dyadic.Thermal.blend line 51

    Source documentation

    cosine series Taylor argument

    private def blend (A : Form M) (y : Grid M) := ∑ i, A i * wave i y

    Mentions: OAI.FourierLLogL.Dyadic.Thermal.Form, OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.Thermal.wave

  8. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_even line 53
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_boltz line 54
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_spec line 59
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_ac_nonneg line 64
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_ac_pos line 71
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_pow_even line 80
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_pow_ac_nonneg line 83
  15. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_pow_ac_pos line 91
  16. def OAI.FourierLLogL.Dyadic.Thermal.aprox line 105

    Source documentation

    Exp series truncated.

    def aprox (n : ℕ) (v : ℝ) := ∑ i ∈ Finset.range n, (i.factorial:ℝ)⁻¹*v^i
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.aprox_lim line 107
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.ac_lim line 111
  19. lemma OAI.FourierLLogL.Dyadic.Thermal.blend_part_le_exp line 121
  20. lemma OAI.FourierLLogL.Dyadic.Thermal.q_nonneg line 132
  21. lemma OAI.FourierLLogL.Dyadic.Thermal.q_pos_one line 138
  22. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_nonneg line 147
  23. lemma OAI.FourierLLogL.Dyadic.Thermal.norm_fc_translate_boltz line 150
  24. lemma OAI.FourierLLogL.Dyadic.Thermal.envelope line 158