OAI/Geometry/PinnedDistances/ExtremalCore.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WeakPinned.Core.Fibers line 36
  2. def OAI.WeakPinned.Core.Fibers.size line 45
  3. def OAI.WeakPinned.Core.Fibers.contribution line 47
  4. def OAI.WeakPinned.Core.Fibers.score line 50
  5. def OAI.WeakPinned.Core.Fibers.active line 52
  6. instance OAI.WeakPinned.Core.Fibers.(instance at line 55) line 55
  7. def OAI.WeakPinned.Core.Fibers.edge line 57
  8. instance OAI.WeakPinned.Core.Fibers.(instance at line 60) line 60
  9. def OAI.WeakPinned.Core.Fibers.degree line 62
  10. def OAI.WeakPinned.Core.Fibers.fiberDegree line 65
  11. lemma OAI.WeakPinned.Core.Fibers.size_mono line 72
  12. lemma OAI.WeakPinned.Core.Fibers.size_erase line 76
  13. lemma OAI.WeakPinned.Core.Fibers.contribution_nonneg line 89
  14. lemma OAI.WeakPinned.Core.Fibers.contribution_mono line 94
  15. lemma OAI.WeakPinned.Core.Fibers.contribution_erase_loss line 104
  16. lemma OAI.WeakPinned.Core.Fibers.edge_no_loop line 140
  17. lemma OAI.WeakPinned.Core.Fibers.edge_unique line 145
  18. lemma OAI.WeakPinned.Core.Fibers.sum_fiberDegree line 150
  19. lemma OAI.WeakPinned.Core.Fibers.score_erase_loss line 187
  20. def OAI.WeakPinned.Core.Fibers.penalty line 192
  21. def OAI.WeakPinned.Core.Fibers.objective line 194
  22. theorem OAI.WeakPinned.Core.Fibers.exists_core line 198

    Source documentation

    Constants here are finite numeric bounds on the original extremal scores. The proof is a maximization on subsets, not an assumption of a core.

    theorem exists_core (K a U : ℝ) (hK : 0 ≤ K) (m₀ : ℕ) (hm : m₀ < Fintype.card V)
    (hboundary : ∀ C : Finset V, C.card=m₀ → G.score K C ≤ U*(m₀ : ℝ)*((m₀ : ℝ)-1))
    (hgap : (U-a)*(m₀ : ℝ)*((m₀ : ℝ)-1) < G.objective K a Finset.univ) :
    ∃ C : Finset V, m₀ < C.card ∧ G.objective K a Finset.univ ≤ G.objective K a C ∧
      ∀ v ∈ C, 2*a*((C.card : ℝ)-1) ≤ G.degree K C v := by
…
  23. def OAI.WeakPinned.Core.Fibers.edgeSet line 237
  24. lemma OAI.WeakPinned.Core.Fibers.edge_indicator line 241
  25. lemma OAI.WeakPinned.Core.Fibers.edgeSet_card line 258
  26. lemma OAI.WeakPinned.Core.Fibers.contribution_formula line 285
  27. lemma OAI.WeakPinned.Core.Fibers.score_le_edgeSet line 294
  28. lemma OAI.WeakPinned.Core.Fibers.score_univ_lower line 302
  29. lemma OAI.WeakPinned.Core.Fibers.sum_sizes_le_edgeSet_univ line 310
  30. lemma OAI.WeakPinned.Core.Fibers.number_fibers line 318
  31. def OAI.WeakPinned.fiberIndices line 329
  32. lemma OAI.WeakPinned.index_source_mem line 332
  33. lemma OAI.WeakPinned.index_radius_pos line 338
  34. def OAI.WeakPinned.planarFibers line 344
  35. lemma OAI.WeakPinned.planar_target_iff line 361
  36. lemma OAI.WeakPinned.planar_fiber_card line 365
  37. def OAI.WeakPinned.planeSubset line 395

    Source documentation

    Return from a subset of labelled vertices to the original plane, retaining all distances and its exact cardinality.

    def planeSubset (P : Finset Plane) (C : Finset P) : Finset Plane := C.image Subtype.val

    Mentions: OAI.WeakPinned.Plane

  38. lemma OAI.WeakPinned.planeSubset_card line 397
  39. lemma OAI.WeakPinned.restricted_targets_subset line 400
  40. lemma OAI.WeakPinned.core_edge_rich line 416
  41. lemma OAI.WeakPinned.subtype_pair_injective line 444
  42. lemma OAI.WeakPinned.core_edge_card line 451
  43. lemma OAI.WeakPinned.core_score_bound line 461
  44. lemma OAI.WeakPinned.initial_edge_image line 474
  45. lemma OAI.WeakPinned.initial_edge_card line 525
  46. lemma OAI.WeakPinned.initial_score_lower line 529
  47. lemma OAI.WeakPinned.index_card_bound line 537
  48. lemma OAI.WeakPinned.initial_score_rate line 547
  49. theorem OAI.WeakPinned.finite_extremal_core line 573

    Source documentation

    A finite actual planar core. All hypotheses before the conclusion are scalar extremal bounds; the graph, degrees and surviving fibers are constructed, not postulated.

    theorem finite_extremal_core (P : Finset Plane) (s r K θ η : ℝ) (m₀ : ℕ)
    (hn : 2 ≤ P.card) (hm0 : 2 ≤ m₀) (hm : m₀ < P.card)
    (hη : 0 < η) (hK0 : 0 ≤ K) (hK : K < (P.card : ℝ)^s)
    (hloss : K ≤ (η/8)*(P.card : ℝ)^s)
    (hinit : θ-η/8 ≤ pairFraction P s)
    (hboundary : (m₀ : ℝ)*((m₀ : ℝ)-1) ≤ (P.card : ℝ)*((P.card : ℝ)-1)/2)
    (hthreshold : ∀ m : ℕ, m₀ ≤ m → m ≤ P.card → (m : ℝ)^r ≤ K)
    (hext : ∀ m : ℕ, m₀ ≤ m → m ≤ P.card → F m r ≤ θ+η/8) :
    ∃ C : Finset P, m₀ < C.card ∧
      (θ-η)*(C.card : ℝ)*((C.card : ℝ)-1) ≤ ((planarFibers P s).edgeSet K C).card ∧
      (((planarFibers P s).edgeSet K C).card : ℝ) ≤ (θ+η/8)*(C.card : ℝ)*((C.card : ℝ)-1) ∧
      (∀ x ∈ C, 2*(θ-η)*((C.card : ℝ)-1) ≤ (planarFibers P s).degree K C x) := by
…

    Mentions: OAI.WeakPinned.Plane, OAI.WeakPinned.pairFraction, OAI.WeakPinned.F, OAI.WeakPinned.planarFibers