OAI/Probability/SLE/Multipoint/MultipointKernelGraph.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The finite graph elimination used in the capped distance kernel. An edge records one selected inverse-distance factor. Each vertex has at most one outgoing edge, including after deleting a vertex.

  1. def OAI.SLEExactGauge.Multipoint.incidentEdges line 15
  2. def OAI.SLEExactGauge.Multipoint.eraseVertex line 18
  3. def OAI.SLEExactGauge.Multipoint.graphKernel line 21
  4. lemma OAI.SLEExactGauge.Multipoint.measurable_graphKernel line 24
  5. lemma OAI.SLEExactGauge.Multipoint.exists_vertex_incident_card_le_two line 29
  6. lemma OAI.SLEExactGauge.Multipoint.incoming_card_le_erase line 61
  7. lemma OAI.SLEExactGauge.Multipoint.exists_free_vertex_incident_card_le_two line 76

    Source documentation

    The low-incidence vertex can be chosen among the integration variables even when one additional vertex is fixed.

    lemma exists_free_vertex_incident_card_le_two {ι : Type*} [DecidableEq ι]
    (S : Finset ι) (hS : S.Nonempty) (root : ι) (hr : root ∉ S)
    (E : Finset (ι × ι))
    (hends : ∀ e ∈ E, e.1 ∈ insert root S ∧ e.2 ∈ insert root S)
    (hout : ∀ e ∈ E, ∀ f ∈ E, e.1=f.1 → e=f)
    (hloop : ∀ e ∈ E, e.1≠e.2) :
    ∃ v ∈ S, (incidentEdges E v).card ≤ 2 := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.incidentEdges

  8. lemma OAI.SLEExactGauge.Multipoint.eraseVertex_properties line 119
  9. lemma OAI.SLEExactGauge.Multipoint.graphKernel_split_vertex line 137
  10. lemma OAI.SLEExactGauge.Multipoint.graphKernel_erase_update line 147
  11. lemma OAI.SLEExactGauge.Multipoint.incident_edge_section line 155
  12. lemma OAI.SLEExactGauge.Multipoint.incident_kernel_section_le line 168
  13. lemma OAI.SLEExactGauge.Multipoint.graphKernel_section_le line 193
  14. theorem OAI.SLEExactGauge.Multipoint.graphKernel_marginal_le_with_root line 216