OAI/Geometry/Convex/GeneralMahler/Hermite/Pair.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Parseval identities for finite-dimensional Gaussian fields and bilinear pairings.

  1. structure OAI.GeneralMahler.HMode.regular line 14

    Source documentation

    A measurable field with polynomial growth.

    structure regular (f:Rn m→F) : Prop where
…

    Mentions: OAI.GeneralMahler.Rn

  2. lemma OAI.GeneralMahler.HMode.regular.ig line 20
  3. lemma OAI.GeneralMahler.HMode.regular.lin line 23
  4. lemma OAI.GeneralMahler.HMode.regular.add line 26
  5. lemma OAI.GeneralMahler.HMode.regular.smul line 29
  6. lemma OAI.GeneralMahler.HMode.regular.mul line 32
  7. lemma OAI.GeneralMahler.HMode.cof_clm line 37
  8. lemma OAI.GeneralMahler.HMode.cof_form line 41
  9. lemma OAI.GeneralMahler.HMode.cof_bil line 50

    Source comment

    Function of a bilinear form, prove via finite-dimensional basis projections
    lemma cof_bil (hf:regular f) (hg:regular g) (l:E→L[ℝ]F→L[ℝ]ℝ) :
    HasSum (fun a=>l (cof f a) (cof g a)) (∫ x,l (f x) (g x) ∂normal m) := by
…

    Mentions: OAI.GeneralMahler.HMode.regular, OAI.GeneralMahler.HMode.cof, OAI.GeneralMahler.normal

  10. lemma OAI.GeneralMahler.HMode.cof_vec line 64
  11. def OAI.GeneralMahler.HMode.deg line 69

    Source comment

    degree/shift arithmetic
    def deg (a:MI m) := ∑ i,a i
…

    Mentions: OAI.GeneralMahler.HMode.MI

  12. lemma OAI.GeneralMahler.HMode.deg_inc line 71
  13. lemma OAI.GeneralMahler.HMode.dz line 80
  14. lemma OAI.GeneralMahler.HMode.dec_inc line 83
  15. lemma OAI.GeneralMahler.HMode.inc_dec line 89
  16. def OAI.GeneralMahler.HMode.userS line 94
  17. def OAI.GeneralMahler.HMode.incE line 95
  18. lemma OAI.GeneralMahler.HMode.inc_sum line 102
  19. lemma OAI.GeneralMahler.HMode.iDeg line 120
  20. lemma OAI.GeneralMahler.HMode.sum_spectral line 124