Integrable kernels preserve bounded Hölder estimates

Convolution with an integrable scalar kernel preserves both a uniform bound and a Hölder constant, multiplying each by the integral of the kernel norm. This applies to truncated planar Cauchy and Newtonian kernels, and to the normalized smoothing kernels used to pass their estimates from smooth to Hölder data.

theorem TauCeti.indicator_kernel_smul_sub_eq {E : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {K : E → 𝕜} {f : E → F} {c w : E} {r R : ℝ} (hs : Function.support f ⊆ Metric.closedBall c r) (hw : w ∈ Metric.closedBall c R) (z : E) : (Metric.closedBall 0 (r + R)).indicator K z • f (w - z) = K z • f (w - z)

A kernel cutoff at the sum of the support and output radii leaves its convolution integrand unchanged on the output disc.

theorem TauCeti.integrable_kernel_smul_sub {E : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {K : E → 𝕜} {f : E → F} {M : ℝ} [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] {μ : MeasureTheory.Measure E} (hK : MeasureTheory.Integrable K μ) (hf : Continuous f) (hM : ∀ (x : E), ‖f x‖ ≤ M) (w : E) : MeasureTheory.Integrable (fun (z : E) => K z • f (w - z)) μ

A bounded continuous function is integrable against every translate of an integrable scalar kernel.

theorem TauCeti.norm_integral_kernel_smul_sub_le {E : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] {K : E → 𝕜} {f : E → F} {M : ℝ} [MeasurableSpace E] {μ : MeasureTheory.Measure E} (hK : MeasureTheory.Integrable K μ) (hM : ∀ (x : E), ‖f x‖ ≤ M) (w : E) : ‖∫ (z : E), K z • f (w - z) ∂μ‖ ≤ (∫ (z : E), ‖K z‖ ∂μ) * M

An integrable scalar kernel multiplies the uniform bound by its L¹ norm.

theorem TauCeti.holderWith_integral_kernel_smul_sub {E : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] {K : E → 𝕜} {f : E → F} [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F] {μ : MeasureTheory.Measure E} (hK : MeasureTheory.Integrable K μ) {H α : NNReal} (hα : 0 < α) (hf : HolderWith H α f) : HolderWith ((∫ (z : E), ‖K z‖ ∂μ).toNNReal * H) α fun (w : E) => ∫ (z : E), K z • f (w - z) ∂μ

An integrable scalar kernel preserves a Hölder exponent and multiplies its constant by its L¹ norm. No boundedness is needed: the Hölder condition makes any two translates of the integrand differ by an integrable function, so either every convolution integral is well-defined or none is, and then all of them vanish.