The normalized positive-kernel bound for the double layer

The double-layer kernel in the Crouzeix--Palencia argument has total mass 4 * pi • 1, while the contour representation of the symmetrized operator has the real normalization factor (2 * pi)⁻¹. Contractivity of integration against a positive operator kernel therefore gives the sharp factor 2.

This file records precisely that scaling step. The positivity, integrability, and mass identity remain explicit inputs, so the theorem can be applied after the geometric and Cauchy-integral parts of the argument have identified the concrete double-layer kernel.

Main declaration

• norm_inv_two_pi_smul_intervalIntegral_le_two_mul_of_nonneg -- a positive kernel of mass 4 * pi • 1, normalized by (2 * pi)⁻¹, integrates every scalar weight bounded by M to an operator of norm at most 2 * M.

theorem norm_inv_two_pi_smul_intervalIntegral_le_two_mul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {K : ℝ → E →L[ℂ] E} {f : ℝ → ℂ} {M : ℝ} (hK : IntervalIntegrable K MeasureTheory.volume 0 (2 * Real.pi)) (hfK : IntervalIntegrable (fun (t : ℝ) => f t • K t) MeasureTheory.volume 0 (2 * Real.pi)) (hpos : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), 0 ≤ K t) (hnorm : ∫ (t : ℝ) in 0..2 * Real.pi, K t = (4 * Real.pi) • 1) (hM : 0 ≤ M) (hf : ∀ t ∈ Set.Ioc 0 (2 * Real.pi), ‖f t‖ ≤ M) : ‖(2 * Real.pi)⁻¹ • ∫ (t : ℝ) in 0..2 * Real.pi, f t • K t‖ ≤ 2 * M

The sharp factor-two scaling of positive-kernel contractivity for a double-layer kernel with total mass 4 * pi • 1.