FiniteRealProductKernel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable finite products of locally finite real kernels

Only finite products of real kernels are needed for the root coordinates. The construction uses binary kernel products and the standard finite coordinate equivalences.

theorem OAI.DukePrimeDegree.exists_finRealProductKernel line 18

theorem OAI.DukePrimeDegree.exists_realProductKernel line 42

Source documentation

A finite product of s-finite real kernels with sigma-finite values is again a kernel, with the expected product measure at every point.

theorem exists_realProductKernel {A I : Type*} [MeasurableSpace A] [Fintype I]
    (κ : I → Kernel A ℝ) [∀ i, IsSFiniteKernel (κ i)]
    [∀ i x, SigmaFinite (κ i x)] :
    ∃ η : Kernel A (I → ℝ), IsSFiniteKernel η ∧
      ∀ x, η x = Measure.pi (fun i => κ i x) := by
…