OAI/Geometry/PinnedDistances/IncomingFibers.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPinned.Core.Fibers.edges line 35
2. def OAI.WeakPinned.Core.Fibers.edgeCount line 37
3. def OAI.WeakPinned.Core.Fibers.edgeLaw line 39
4. def OAI.WeakPinned.Core.Fibers.fiberWeight line 41
5. def OAI.WeakPinned.Core.Fibers.incoming line 43
6. def OAI.WeakPinned.Core.Fibers.incomingWeight line 45
7. lemma OAI.WeakPinned.Core.Fibers.active_univ_neg_one line 48
8. lemma OAI.WeakPinned.Core.Fibers.edgeCount_eq line 53
9. lemma OAI.WeakPinned.Core.Fibers.edgeLaw_nonneg line 59
10. lemma OAI.WeakPinned.Core.Fibers.edgeLaw_diag line 64
11. lemma OAI.WeakPinned.Core.Fibers.fiberWeight_nonneg line 71
12. lemma OAI.WeakPinned.Core.Fibers.sum_fiberWeight line 75
13. lemma OAI.WeakPinned.Core.Fibers.fiberWeight_prob line 79
14. lemma OAI.WeakPinned.Core.Fibers.sampling_fiber line 88
15. lemma OAI.WeakPinned.Core.Fibers.fiber_marginal line 102
16. lemma OAI.WeakPinned.Core.Fibers.incoming_marginal line 111
17. lemma OAI.WeakPinned.Core.Fibers.sampling_incoming line 116
18. lemma OAI.WeakPinned.Core.Fibers.sum_edgeLaw line 127
19. lemma OAI.WeakPinned.Core.Fibers.sum_incomingWeight line 136
20. lemma OAI.WeakPinned.Core.Fibers.fiber_domination line 140
21. lemma OAI.WeakPinned.Core.Fibers.incoming_domination line 148
22. lemma OAI.WeakPinned.Core.Fibers.small_incoming_mass line 158

    Source documentation

    The exact bound on omitted small incoming degrees, not just a formal little-o assertion.

    lemma small_incoming_mass (T : ℝ) (hT : 0 ≤ T) :
        (∑ y, if ((G.incoming y).card : ℝ)<T then G.incomingWeight y else 0) ≤
          (Fintype.card V : ℝ)*T/G.edgeCount := by
    …

23. abbrev OAI.WeakPinned.Core.Fibers.Active line 177
24. instance OAI.WeakPinned.Core.Fibers.(instance at line 179) line 179
25. def OAI.WeakPinned.Core.Fibers.onCore line 183
26. lemma OAI.WeakPinned.Core.Fibers.onCore_targets line 196
27. lemma OAI.WeakPinned.Core.Fibers.onCore_size line 205
28. lemma OAI.WeakPinned.Core.Fibers.onCore_edge line 211
29. lemma OAI.WeakPinned.Core.Fibers.onCore_edges_image line 222
30. lemma OAI.WeakPinned.Core.Fibers.onCore_card line 237
31. lemma OAI.WeakPinned.Core.Fibers.onCore_degree line 245
32. lemma OAI.WeakPinned.Core.Fibers.onCore_size_subset line 270
33. def OAI.WeakPinned.Core.Fibers.heavyCount line 283
34. lemma OAI.WeakPinned.Core.Fibers.onCore_heavyCount line 288
35. lemma OAI.WeakPinned.Core.Fibers.degree_marginal line 311
36. abbrev OAI.WeakPinned.coreGraph line 322
37. lemma OAI.WeakPinned.coreGraph_heavy line 325
38. structure OAI.WeakPinned.PreparedGraph line 333
39. lemma OAI.WeakPinned.PreparedCore.graph line 344
40. theorem OAI.WeakPinned.arbitrarily_large_graph line 369

    Source documentation

    Actual arbitrarily large real planar graphs, with all uniform subset bounds simultaneously. No graph condition is added to the main hypothesis.

    theorem arbitrarily_large_graph (hfail : ¬ MainStatement) {s γ c : ℝ}
        (hγ : 0<γ) (hγs : γ<s) (hc : 0<c) (hc1 : c<1)
        (hsc : (1-c)*criticalExponent<s) (hs : ContinuousAt Theta s)
        (η : ℝ) (hη : 0<η) (M : ℕ) :
        ∃ (P : Finset Plane) (C : Finset P), M<C.card ∧
          PreparedGraph C ((planarFibers P s).Active (cutoff s P.card) C) (coreGraph P s C) (Theta s) γ c η := by
    …

    Mentions: OAI.WeakPinned.MainStatement, OAI.WeakPinned.criticalExponent, OAI.WeakPinned.Theta, OAI.WeakPinned.Plane, OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.planarFibers, OAI.WeakPinned.cutoff, OAI.WeakPinned.coreGraph