OAI/Geometry/Convex/GeneralMahler/MixedField.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Layer integrals and error estimates.

  1. lemma OAI.GeneralMahler.mixed_integral_right line 13
  2. def OAI.GeneralMahler.ProjField.Gstep line 35
  3. def OAI.GeneralMahler.ProjField.Pstep line 36
  4. def OAI.GeneralMahler.ProjField.PD line 37
  5. lemma OAI.GeneralMahler.ProjField.meas_XT line 39
  6. lemma OAI.GeneralMahler.ProjField.meas_YT line 44
  7. lemma OAI.GeneralMahler.ProjField.Pstep_sm line 48
  8. lemma OAI.GeneralMahler.ProjField.PD_sm line 55
  9. lemma OAI.GeneralMahler.ProjField.one_op_le line 64
  10. lemma OAI.GeneralMahler.ProjField.Pstep_norm line 69
  11. lemma OAI.GeneralMahler.ProjField.uniform_Pstep line 77
  12. lemma OAI.GeneralMahler.ProjField.Pstep_mixed line 106
  13. lemma OAI.GeneralMahler.ProjField.mixed_PD line 112
  14. lemma OAI.GeneralMahler.ProjField.tail_H line 122

    Source comment

    h minus its step decays rapidly
    lemma tail_H : rapid (fun z : ℝ => q.avH z - st z * q.s0) := by
…

    Mentions: OAI.GeneralMahler.rapid