High-contrast homogenization: Provider.PolynomialHomogenization.WeightedNonnegativeKernelSchur

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

A weighted Schur test for nonnegative kernels

This is the conjugated form of the nonnegative-kernel Schur test. Separate positive finite weights on the source and target permit row and column bounds that scale with distance to a boundary.

theorem HCPolySupport.HighContrast.lintegral_weightedNonnegativeKernel_rpow_two_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] {K : α → β → ENNReal} {f : β → ENNReal} {p : α → ENNReal} {q : β → ENNReal} {A B : ENNReal} (hK : Measurable (Function.uncurry K)) (hf : Measurable f) (hp : Measurable p) (hq : Measurable q) (hq0 : ∀ (y : β), q y ≠ 0) (hqtop : ∀ (y : β), q y ≠ ⊤) (hrow : ∀ᵐ (x : α) ∂μ, ∫⁻ (y : β), K x y * q y ∂ν ≤ A * p x) (hcol : ∀ᵐ (y : β) ∂ν, ∫⁻ (x : α), K x y * p x ∂μ ≤ B * q y) : ∫⁻ (x : α), (∫⁻ (y : β), K x y * f y ∂ν) ^ 2 ∂μ ≤ A * B * ∫⁻ (y : β), f y ^ 2 ∂ν

Weighted squared L² Schur test. The target weight p and source weight q need only be positive and finite; no integrability hypothesis on the input is required.