OAI/Geometry/Convex/GeneralMahler/ProjMean.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Biased projection lemma §02: mean derivative

  1. def OAI.GeneralMahler.projJac line 15

    Source documentation

    Projection Jacobian, zero at undefined points.

    def projJac (x : (Rn m)) : Mat m := op.symm (fderiv ℝ (coneProj C) x)

    Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.Mat, OAI.GeneralMahler.coneProj

  2. lemma OAI.GeneralMahler.projJac_op line 17
  3. lemma OAI.GeneralMahler.projJac_sym line 20
  4. lemma OAI.GeneralMahler.projJac_pos line 23
  5. lemma OAI.GeneralMahler.projJac_norm line 27
  6. lemma OAI.GeneralMahler.projJac_le_one line 31
  7. lemma OAI.GeneralMahler.projJac_id line 34
  8. lemma OAI.GeneralMahler.projJac_zero line 43
  9. lemma OAI.GeneralMahler.strongly_projJac line 51
  10. def OAI.GeneralMahler.affineN line 58
  11. lemma OAI.GeneralMahler.continuous_affineN line 59
  12. lemma OAI.GeneralMahler.tendsto_ae_affineN line 62
  13. lemma OAI.GeneralMahler.affineN_integrable line 72
  14. lemma OAI.GeneralMahler.affineN_mean line 76
  15. def OAI.GeneralMahler.sample line 89
  16. lemma OAI.GeneralMahler.continuous_sample line 91
  17. lemma OAI.GeneralMahler.poly_sample line 94
  18. lemma OAI.GeneralMahler.sample_integrable line 98
  19. def OAI.GeneralMahler.mean line 101
  20. def OAI.GeneralMahler.meanJac line 102
  21. lemma OAI.GeneralMahler.meanJac_integrable line 104
  22. theorem OAI.GeneralMahler.hasFDerivAt_mean line 110
  23. theorem OAI.GeneralMahler.mean_C_one line 138
  24. lemma OAI.GeneralMahler.prob_open line 156

    Source comment

    strict inequalities for the average derivative
    lemma prob_open (a : (Rn m)) (s : Set (Rn m)) (hs : IsOpen s) (he : s.Nonempty) :
    0 < normal m ((affineN B a) ⁻¹' s) := by
…

    Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.normal, OAI.GeneralMahler.affineN

  25. lemma OAI.GeneralMahler.strict_pos_of_layer line 164
  26. theorem OAI.GeneralMahler.mean_pos line 178
  27. theorem OAI.GeneralMahler.mean_lt_one line 183