OAI/Probability/SLE/Multipoint/MultipointFixedCenterKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed-center form of the capped kernel estimate. The constant is independent of the location of the fixed center.

  1. def OAI.SLEExactGauge.Multipoint.fixedKernelBound line 15
  2. lemma OAI.SLEExactGauge.Multipoint.fixedKernelBound_lt_top line 18
  3. lemma OAI.SLEExactGauge.Multipoint.cappedDistanceKernel_marginal_le line 25
  4. lemma OAI.SLEExactGauge.Multipoint.lintegral_fin_cons_eq_marginal line 66
  5. theorem OAI.SLEExactGauge.Multipoint.cappedDistanceKernel_fixed_center_bound line 105

    Source documentation

    Uniform fixed-center kernel bound, with the center in coordinate zero and the free variables in the successor coordinates.

    theorem cappedDistanceKernel_fixed_center_bound (m : ℕ)
    {α : ℝ} (hα : 0 < α) (hα1 : α < 1) (b : ℝ)
    (K : Set ℂ) (hK : Bornology.IsBounded K) :
    ∃ C : ℝ≥0∞, C < ⊤ ∧ ∀ z : ℂ,
      (∫⁻ x, cappedDistanceKernel α b (Fin.cons z x)
        ∂Measure.pi (fun _ : Fin m => volume.restrict K)) ≤ C := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.cappedDistanceKernel

  6. lemma OAI.SLEExactGauge.Multipoint.ae_fin_cons_injective line 117