Assembly of the symmetrized double-layer bound #
This file packages the last norm-estimate step of L4.2d. Once an operator
sum F + G† has been represented as the (2 * pi)⁻¹-normalized integral of
a scalar weight against a positive operator kernel of total mass
4 * pi • 1, positive-kernel contractivity gives the sharp estimate
norm (F + G†) ≤ 2 * M.
All analytic and geometric inputs remain visible in the theorem statement:
the representation, interval integrability, positivity, mass normalization,
and scalar boundary bound. The theorem therefore composes directly with a
Cauchy representation of p(A) + G† without asserting that missing identity
itself.
Main declaration #
norm_add_star_le_two_mul_of_doubleLayer_representation-- the final factor-two norm estimate from a normalized positive double-layer representation.
theorem
norm_add_star_le_two_mul_of_doubleLayer_representation
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℂ E]
[CompleteSpace E]
(F G : E →L[ℂ] E)
{K : ℝ → E →L[ℂ] E}
{f : ℝ → ℂ}
{M : ℝ}
(hrepresentation : F + star G = (2 * Real.pi)⁻¹ • ∫ (t : ℝ) in 0..2 * Real.pi, f t • K t)
(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)
:
An explicit normalized positive double-layer representation of F + G†
implies the sharp bound ‖F + G†‖ ≤ 2 * M.