Kernel Positivity-Improving Criterion

An integral operator Tf(x) = ∫ K(x,y) f(y) dμ(y) on L²(Ω, μ) is positivity-improving if and only if K(x,y) > 0 for μ ⊗ μ-a.e. (x,y).

Proof strategy

Forward direction (K > 0 a.e. → T positivity-improving): If f ≥ 0, f ≠ 0, then f > 0 on a set S of positive measure. Tf(x) = ∫ K(x,y) f(y) dμ(y) ≥ ∫_S K(x,y) f(y) dμ(y) > 0 for a.e. x, since K(x,·) > 0 a.e. and f > 0 on S.

Reverse direction (T positivity-improving → K > 0 a.e.): For any measurable sets A, B of positive measure, ⟨1_A, T(1_B)⟩ = ∫∫_{A×B} K(x,y) dμ(x)dμ(y) > 0 (since T(1_B) > 0 a.e., in particular on A). This forces K > 0 a.e. on A × B for all such A, B.

References

• Reed–Simon IV, Theorem XIII.44
• Simon, Functional Integration and Quantum Physics, Prop. I.12

structure IntegralOperator (Ω : Type u_2) [MeasureTheory.MeasureSpace Ω] : Type u_2

An integral operator on L² defined by a kernel K : Ω × Ω → ℝ. Tf(x) = ∫ K(x,y) f(y) dμ(y).

• kernel : Ω → Ω → ℝ

  The integral kernel K : Ω → Ω → ℝ of the operator.

• kernel_measurable : Measurable (Function.uncurry self.kernel)

  The kernel, viewed as a function on Ω × Ω, is measurable.

def IntegralOperator.IsAEPositive {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (T : IntegralOperator Ω) : Prop

A kernel is a.e. positive if K(x,y) > 0 for (volume ⊗ volume)-a.e. (x,y).

Equations

• T.IsAEPositive = ∀ᵐ (p : Ω × Ω) ∂MeasureTheory.volume.prod MeasureTheory.volume, 0 < T.kernel p.1 p.2

theorem IntegralOperator.ae_pos_integral_of_ae_pos_kernel {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.SFinite MeasureTheory.volume] (T : IntegralOperator Ω) (hK : T.IsAEPositive) (f : Ω → ℝ) (_hf_meas : Measurable f) (hf_nonneg : ∀ᵐ (x : Ω), 0 ≤ f x) (hf_ne : ¬f =ᵐ[MeasureTheory.volume] 0) (hf_int : ∀ᵐ (x : Ω), MeasureTheory.Integrable (fun (y : Ω) => T.kernel x y * f y) MeasureTheory.volume) : ∀ᵐ (x : Ω), 0 < ∫ (y : Ω), T.kernel x y * f y

Forward direction: if K(x,y) > 0 a.e. and f ≥ 0, f ≠ 0, then Tf(x) = ∫ K(x,y) f(y) dμ(y) > 0 for a.e. x.

theorem IntegralOperator.ae_pos_kernel_of_positivity_improving {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.SFinite MeasureTheory.volume] [MeasurableSingletonClass Ω] (T : IntegralOperator Ω) (h_atom_pos : ∀ (x : Ω), 0 < MeasureTheory.volume {x}) (h_atom_fin : ∀ (x : Ω), MeasureTheory.volume {x} ≠ ⊤) (hT : ∀ (A B : Set Ω), MeasurableSet A → MeasurableSet B → 0 < MeasureTheory.volume A → 0 < MeasureTheory.volume B → 0 < ∫ (x : Ω) in A, ∫ (y : Ω) in B, T.kernel x y) : T.IsAEPositive

Reverse direction in the purely atomic case: if singletons are measurable with positive finite measure and every positive-measure pair (A, B) has strictly positive double integral, then K(x, y) > 0 for every pair (x, y), hence in particular for a.e. (x, y).