OAI/Geometry/Convex/GeneralMahler/Linear/SpectralIBP.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

§06 Gaussian spectral averaging functional. Eq24 in normalized trace pairing.

  1. lemma OAI.GeneralMahler.reg_constM line 11
  2. lemma OAI.GeneralMahler.int_Pj line 13
  3. def OAI.GeneralMahler.ProjField.sumS line 19
  4. def OAI.GeneralMahler.ProjField.locR line 20
  5. def OAI.GeneralMahler.ProjField.RM line 23
  6. lemma OAI.GeneralMahler.ProjField.DRi line 26
  7. lemma OAI.GeneralMahler.ProjField.dl_again line 31
  8. lemma OAI.GeneralMahler.ProjField.xf_reg line 38
  9. lemma OAI.GeneralMahler.ProjField.dl_identity line 42
  10. lemma OAI.GeneralMahler.ProjField.coord_pb line 55
  11. lemma OAI.GeneralMahler.ProjField.L_identity line 67

    Source comment

    the evaluation weighted by W
    lemma L_identity {f:ℝ→ℝ} (hf:TestF f) :
    etw W (fun x:Rn m=> q.Lmat x*q.FL.eval f x) =
      ∑ i:Fin m, (∫ x,Pj W (q.M i) (q.DLMat (deriv f) x i) ∂normal m) := by
…

    Mentions: OAI.GeneralMahler.TestF, OAI.GeneralMahler.etw, OAI.GeneralMahler.Rn, OAI.GeneralMahler.Pj, OAI.GeneralMahler.normal

  12. lemma OAI.GeneralMahler.ProjField.RM_Form line 89
  13. lemma OAI.GeneralMahler.ProjField.W_int line 104
  14. lemma OAI.GeneralMahler.ProjField.eq24 line 110