MultipointKernelExpansion.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Each term of the nearest-neighbor cap expansion is a loop-free graph with at most one outgoing edge at every vertex. Integrating a vertex of incidence at most two proves the fixed-order kernel estimate.

def OAI.SLEExactGauge.Multipoint.selectedTarget line 15
def OAI.SLEExactGauge.Multipoint.selectedVertices line 17
def OAI.SLEExactGauge.Multipoint.selectedEdges line 20
lemma OAI.SLEExactGauge.Multipoint.selectedEdges_outgoing line 23
lemma OAI.SLEExactGauge.Multipoint.selectedEdges_loopfree line 31
lemma OAI.SLEExactGauge.Multipoint.graphKernel_selectedEdges line 37
def OAI.SLEExactGauge.Multipoint.capCoefficient line 50
lemma OAI.SLEExactGauge.Multipoint.capCoefficient_finite line 52
lemma OAI.SLEExactGauge.Multipoint.rowChoice_le_graph_factor line 56
lemma OAI.SLEExactGauge.Multipoint.rowProduct_le_graph line 75
lemma OAI.SLEExactGauge.Multipoint.cappedDistanceKernel_le_graph_sum line 82

theorem OAI.SLEExactGauge.Multipoint.graphKernel_marginal_le line 90

Source documentation

Integrate all graph vertices. The empty index set is included.

theorem graphKernel_marginal_le {ι : Type*} [DecidableEq ι]
    (α : ℝ) (K : Set ℂ) (C : ℝ≥0∞) (hC : C < ⊤)
    (hC0 : volume K ≤ C)
    (hC1 : ∀ y, (∫⁻ x in K, distanceKernel α x y) ≤ C)
    (hC2 : ∀ y z, (∫⁻ x in K, distanceKernel α x y * distanceKernel α x z) ≤ C)
    (S : Finset ι) (E : Finset (ι × ι))
    (hends : ∀ e ∈ E, e.1 ∈ S ∧ e.2 ∈ S)
    (hout : ∀ e ∈ E, ∀ f ∈ E, e.1=f.1 → e=f)
    (hloop : ∀ e ∈ E, e.1≠e.2) (x : ι → ℂ) :
    lmarginal (fun _ : ι => volume.restrict K) S (graphKernel α E) x ≤ C^S.card := by
…

Mentions: OAI.SLEExactGauge.Multipoint.distanceKernel, OAI.SLEExactGauge.Multipoint.graphKernel

lemma OAI.SLEExactGauge.Multipoint.selectedGraph_integral_le line 127
theorem OAI.SLEExactGauge.Multipoint.cappedDistanceKernel_integral_lt_top line 142
Source documentation
The exact capped inverse-distance kernel has a finite integral on every bounded planar product set, for every fixed order.
```
theorem cappedDistanceKernel_integral_lt_top {ι : Type*} [Fintype ι] [DecidableEq ι]
    {α : ℝ} (hα : 0 < α) (hα1 : α < 1) (b : ℝ)
    (K : Set ℂ) (hK : Bornology.IsBounded K) :
    (∫⁻ x, cappedDistanceKernel (ι := ι) α b x
…
```
Mentions: OAI.SLEExactGauge.Multipoint.cappedDistanceKernel