OAI/Geometry/Convex/GeneralMahler/BoundField.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Uniform cone hypotheses for the full-real-line estimates. The extra constants are not inputs to main theorems: for every field such bounds exist.

  1. structure OAI.GeneralMahler.ProjField.Bound line 15
  2. lemma OAI.GeneralMahler.ProjField.Bound.positive line 27
  3. theorem OAI.GeneralMahler.ProjField.Field_isBound line 30
  4. lemma OAI.GeneralMahler.ProjField.Bound.normZ line 58
  5. lemma OAI.GeneralMahler.ProjField.X_int line 65
  6. lemma OAI.GeneralMahler.ProjField.Y_int line 66
  7. lemma OAI.GeneralMahler.ProjField.avH_le_s line 70
  8. lemma OAI.GeneralMahler.ProjField.Bt_cd line 80
  9. lemma OAI.GeneralMahler.ProjField.m_pos line 88
  10. lemma OAI.GeneralMahler.ProjField.Bound.s0_le line 91
  11. lemma OAI.GeneralMahler.ProjField.Bound.X_mean line 108
  12. lemma OAI.GeneralMahler.ProjField.Bound.Y_mean line 123
  13. lemma OAI.GeneralMahler.ProjField.mul_Bt_avH line 136
  14. lemma OAI.GeneralMahler.ProjField.XT_lip' line 142
  15. lemma OAI.GeneralMahler.ProjField.YT_lip' line 153
  16. def OAI.GeneralMahler.ProjField.J line 162
  17. lemma OAI.GeneralMahler.ProjField.i_norm line 164
  18. lemma OAI.GeneralMahler.ProjField.j_nonneg line 166
  19. lemma OAI.GeneralMahler.ProjField.norm_le_mean_error line 169

    Source comment

    Bounding a Lipschitz map by its mean absolute norm
    lemma norm_le_mean_error {E:Type*} [NormedAddCommGroup E] {F : Rn m → E} {K : ℝ}
    (hf : Integrable F (normal m)) (hl : ∀ x y, ‖F x - F y‖ ≤ K*‖x-y‖)
    (hk : 0 ≤ K) (x : Rn m) :
    ‖F x‖ ≤ (∫ x, ‖F x‖ ∂normal m)+ K*(‖x‖+J m) := by
…

    Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.normal, OAI.GeneralMahler.ProjField.J