Contractivity of integration against a positive operator kernel (L4.2d support)

If K t is a positive operator for t ∈ (a, b] and ∫ t in a..b, K t = c • 1, then integrating a bounded scalar weight f against K is contractive up to the mass c: ‖∫ t in a..b, f t • K t‖ ≤ c * sup ‖f‖. This is the bridge from the pointwise positivity of the double-layer kernel (DoubleLayer.lean, PositiveIntegral.lean) to the sharp symmetrized bound of Crouzeix–Palencia: the raw double-layer kernel has total mass 4π (DoubleLayerIntegral.lean), so after the 1 / (2π) normalization of the contour integral the estimate carries the factor 2.

Route: for a positive K, ⟪x, K y⟫ = ⟪√K x, √K y⟫, hence ‖⟪x, K y⟫‖ ≤ √(re ⟪x, K x⟫) * √(re ⟪y, K y⟫) (Cauchy–Schwarz for the positive form); the weighted AM–GM inequality √A * √B ≤ (s * A + B / s) / 2 turns this into an integrable majorant with integral M * ((s * c * ‖x‖ ^ 2 + c * ‖y‖ ^ 2 / s) / 2); optimizing s = ‖y‖ / ‖x‖ gives ‖⟪x, T y⟫‖ ≤ c * M * ‖x‖ * ‖y‖, and an operator with such matrix coefficients has norm at most c * M.

Main declarations

• norm_inner_apply_le_sqrt_mul_sqrt_of_nonneg — Cauchy–Schwarz for a positive operator, via the continuous-functional-calculus square root (inner_apply_eq_inner_cfcSqrt_of_nonneg).
• opNorm_le_of_forall_norm_inner_le — an operator norm bound from a matrix-coefficient bound.
• sqrt_mul_sqrt_le_of_pos, norm_inner_le_of_forall_pos_le — the scalar AM–GM step and its optimization.
• norm_intervalIntegral_smul_le_of_ae_nonneg — the contractivity bound ‖∫ t in a..b, f t • K t‖ ≤ c * M (hypotheses almost everywhere on Ioc a b), and its pointwise form norm_intervalIntegral_smul_le_of_nonneg.

Requires [CompleteSpace E] for the square root of a positive operator and for the operator-valued Bochner integrals.

theorem inner_apply_eq_inner_cfcSqrt_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {K : E →L[ℂ] E} (hK : 0 ≤ K) (x y : E) : inner ℂ x (K y) = inner ℂ ((CFC.sqrt K) x) ((CFC.sqrt K) y)

For a positive operator K, ⟪x, K y⟫ = ⟪√K x, √K y⟫.

theorem re_inner_apply_self_eq_norm_cfcSqrt_sq_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {K : E →L[ℂ] E} (hK : 0 ≤ K) (x : E) : RCLike.re (inner ℂ x (K x)) = ‖(CFC.sqrt K) x‖ ^ 2

For a positive operator K, re ⟪x, K x⟫ = ‖√K x‖ ^ 2.

theorem norm_inner_apply_le_sqrt_mul_sqrt_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {K : E →L[ℂ] E} (hK : 0 ≤ K) (x y : E) : ‖inner ℂ x (K y)‖ ≤ √(RCLike.re (inner ℂ x (K x))) * √(RCLike.re (inner ℂ y (K y)))

Cauchy–Schwarz for a positive operator: ‖⟪x, K y⟫‖ ≤ √(re ⟪x, K x⟫) * √(re ⟪y, K y⟫).

theorem opNorm_le_of_forall_norm_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {T : E →L[ℂ] E} {M : ℝ} (hM : 0 ≤ M) (h : ∀ (x y : E), ‖inner ℂ x (T y)‖ ≤ M * ‖x‖ * ‖y‖) : ‖T‖ ≤ M

An operator whose matrix coefficients are bounded by M * ‖x‖ * ‖y‖ has norm at most M.

theorem sqrt_mul_sqrt_le_of_pos {A B s : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hs : 0 < s) : √A * √B ≤ (s * A + B / s) / 2

Weighted AM–GM: √A * √B ≤ (s * A + B / s) / 2 for A, B ≥ 0 and s > 0.

theorem norm_inner_le_of_forall_pos_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {T : E →L[ℂ] E} {c M : ℝ} (x y : E) (h : ∀ (s : ℝ), 0 < s → ‖inner ℂ x (T y)‖ ≤ M * ((s * (c * ‖x‖ ^ 2) + c * ‖y‖ ^ 2 / s) / 2)) : ‖inner ℂ x (T y)‖ ≤ c * M * ‖x‖ * ‖y‖

If ‖⟪x, T y⟫‖ ≤ M * ((s * (c ‖x‖²) + c ‖y‖² / s) / 2) for every s > 0, then ‖⟪x, T y⟫‖ ≤ c * M * ‖x‖ * ‖y‖.

theorem norm_intervalIntegral_smul_le_of_ae_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {K : ℝ → E →L[ℂ] E} {f : ℝ → ℂ} {a b c M : ℝ} (hab : a ≤ b) (hK : IntervalIntegrable K MeasureTheory.volume a b) (hfK : IntervalIntegrable (fun (t : ℝ) => f t • K t) MeasureTheory.volume a b) (hpos : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), 0 ≤ K t) (hnorm : ∫ (t : ℝ) in a..b, K t = c • 1) (hc : 0 ≤ c) (hM : 0 ≤ M) (hf : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), ‖f t‖ ≤ M) : ‖∫ (t : ℝ) in a..b, f t • K t‖ ≤ c * M

Contractivity of integration against a normalized positive operator kernel. If K t ≥ 0 almost everywhere on Ioc a b, ∫ t in a..b, K t = c • 1, and ‖f t‖ ≤ M almost everywhere on Ioc a b, then ‖∫ t in a..b, f t • K t‖ ≤ c * M.

theorem norm_intervalIntegral_smul_le_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {K : ℝ → E →L[ℂ] E} {f : ℝ → ℂ} {a b c M : ℝ} (hab : a ≤ b) (hK : IntervalIntegrable K MeasureTheory.volume a b) (hfK : IntervalIntegrable (fun (t : ℝ) => f t • K t) MeasureTheory.volume a b) (hpos : ∀ t ∈ Set.Ioc a b, 0 ≤ K t) (hnorm : ∫ (t : ℝ) in a..b, K t = c • 1) (hc : 0 ≤ c) (hM : 0 ≤ M) (hf : ∀ t ∈ Set.Ioc a b, ‖f t‖ ≤ M) : ‖∫ (t : ℝ) in a..b, f t • K t‖ ≤ c * M

The contractivity bound with pointwise hypotheses on Ioc a b.