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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralMahler.Seg.integral_sq_le line 12
2. lemma OAI.GeneralMahler.Seg.bar_sq line 32
3. def OAI.GeneralMahler.Seg.signE line 38
4. def OAI.GeneralMahler.Seg.rcoef line 39
5. def OAI.GeneralMahler.Seg.Om line 40
6. def OAI.GeneralMahler.Seg.kz line 42
7. lemma OAI.GeneralMahler.Seg.r_swap line 45
8. lemma OAI.GeneralMahler.Seg.K_swap line 50
9. lemma OAI.GeneralMahler.Seg.O_swap line 52
10. lemma OAI.GeneralMahler.Seg.bar_const line 53
11. lemma OAI.GeneralMahler.Seg.middle line 55
12. lemma OAI.GeneralMahler.Seg.av_dist line 87

    Source comment

    parameterized ray ε, near z+ε*b, far z+ε*a.

    lemma av_dist (f:Plane→ℝ) (z sig b:ℝ) (_hb:0<b) :
        bAv f (z,z+sig*b)*b = ∫ t in 0..b,f (z,z+sig*t) := by
    …

    Mentions: OAI.GeneralMahler.Plane, OAI.GeneralMahler.bAv

13. lemma OAI.GeneralMahler.Seg.ext_shape line 97
14. lemma OAI.GeneralMahler.Seg.K_ext line 117

    Source comment

    exterior, parameterized orientation. U replaced analytic RHS.

    lemma K_ext (f:Plane→ℝ) (hf:Bwt f) (z s a b:ℝ) (hs:s=1 ∨ s= -1)
        (hp:0<b) (h:b<a) :
        let x:=z+s*b
    …

    Mentions: OAI.GeneralMahler.Plane, OAI.GeneralMahler.Bwt

15. lemma OAI.GeneralMahler.Seg.k_same line 196
16. lemma OAI.GeneralMahler.Seg.O_nn line 204
17. lemma OAI.GeneralMahler.Seg.pairOrd line 212
18. lemma OAI.GeneralMahler.Seg.pairEst line 228