OAI/Geometry/Convex/GeneralMahler/Segment/Mean.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

§08 segment coordinates and physical averages.

  1. def OAI.GeneralMahler.SCal.SE.left line 12
  2. def OAI.GeneralMahler.SCal.SE.right line 13
  3. def OAI.GeneralMahler.SCal.SE.seg line 14
  4. def OAI.GeneralMahler.SCal.SE.loc line 15
  5. def OAI.GeneralMahler.SCal.SE.mean0 line 16
  6. def OAI.GeneralMahler.SCal.SE.de line 17
  7. def OAI.GeneralMahler.SCal.SE.normM line 18
  8. def OAI.GeneralMahler.SCal.SE.normE line 19
  9. def OAI.GeneralMahler.SCal.SE.Pbar line 20
  10. lemma OAI.GeneralMahler.SCal.SE.mean_const line 22
  11. lemma OAI.GeneralMahler.SCal.SE.mean_add line 24
  12. lemma OAI.GeneralMahler.SCal.SE.mean_sub line 28
  13. lemma OAI.GeneralMahler.SCal.SE.mean_scale line 32
  14. lemma OAI.GeneralMahler.SCal.SE.mean_mono line 34
  15. lemma OAI.GeneralMahler.SCal.SE.mean_ref line 40
  16. lemma OAI.GeneralMahler.SCal.SE.cLoc line 44
  17. lemma OAI.GeneralMahler.SCal.SE.cDe line 45
  18. lemma OAI.GeneralMahler.SCal.SE.normGe line 46
  19. lemma OAI.GeneralMahler.SCal.SE.normp line 49
  20. lemma OAI.GeneralMahler.SCal.SE.neScale line 51
  21. lemma OAI.GeneralMahler.SCal.SE.neConst line 54
  22. lemma OAI.GeneralMahler.SCal.SE.neMono line 58
  23. lemma OAI.GeneralMahler.SCal.SE.neAdd line 65
  24. lemma OAI.GeneralMahler.SCal.SE.neSub line 69
  25. lemma OAI.GeneralMahler.SCal.SE.hsinh line 74
  26. lemma OAI.GeneralMahler.SCal.SE.loct line 76
  27. lemma OAI.GeneralMahler.SCal.SE.nor_eq line 78
  28. lemma OAI.GeneralMahler.SCal.SE.loch_local line 86
  29. lemma OAI.GeneralMahler.SCal.SE.bav_phys line 91

    Source comment

    transfer any continuous f (on all ℝ)
    lemma bav_phys (f:ℝ→ℝ)(hf:Continuous f)(a b:ℝ):
    (b-a)*bav f (a,b) = ∫ t in a..b,f t:=by
…

    Mentions: OAI.GeneralMahler.bav

  30. lemma OAI.GeneralMahler.SCal.SE.normChange line 106
  31. lemma OAI.GeneralMahler.SCal.SE.bav_norm line 135