Coarse-graining support: Support.Sobolev.W1p.ConvolutionLp

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.convexOn_abs_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ Set.univ fun (x : ℝ) => |x| ^ p

The function x ↦ |x|^p is convex on ℝ for p ≥ 1.

theorem HCPolySupport.isProbabilityMeasure_withDensity_ofReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ρ : α → ℝ} (hρ_nonneg : ∀ (x : α), 0 ≤ ρ x) (hρ_int : MeasureTheory.Integrable ρ μ) (hρ_one : ∫ (x : α), ρ x ∂μ = 1) : MeasureTheory.IsProbabilityMeasure (μ.withDensity fun (x : α) => ENNReal.ofReal (ρ x))

A real-valued density of integral 1 yields a probability measure via withDensity.

theorem HCPolySupport.jensen_abs_rpow_integral {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {f : α → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf : MeasureTheory.Integrable f μ) (hfpow : MeasureTheory.Integrable (fun (x : α) => |f x| ^ p) μ) : |∫ (x : α), f x ∂μ| ^ p ≤ ∫ (x : α), |f x| ^ p ∂μ

Jensen's inequality for x ↦ |x|^p against a probability measure.

theorem HCPolySupport.eLpNorm_comp_sub_right {d : ℕ} (f : Vec d → ℝ) (t : Vec d) (p : ENNReal) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (x - t)) p MeasureTheory.volume = MeasureTheory.eLpNorm f p MeasureTheory.volume

Translation invariance of eLpNorm for Lebesgue measure on Vec d.

theorem HCPolySupport.lintegral_comp_sub_right {d : ℕ} (f : Vec d → ENNReal) (hf : Measurable f) (t : Vec d) : ∫⁻ (x : Vec d), f (x - t) = ∫⁻ (x : Vec d), f x

Translation invariance of lintegral for Lebesgue measure on Vec d.

theorem HCPolySupport.fubini_translation_key {d : ℕ} (ρ : Vec d → ENNReal) (g : Vec d → ℝ) (p : ℝ) (hρ : Measurable ρ) (hg : Measurable g) : ∫⁻ (x : Vec d) (t : Vec d), ρ t * ENNReal.ofReal |g (x - t)| ^ p = (∫⁻ (t : Vec d), ρ t) * ∫⁻ (x : Vec d), ENNReal.ofReal |g x| ^ p

Fubini plus translation invariance for the kernel used in the Jensen proof of convolution contraction.

theorem HCPolySupport.young_convolution_nonneg_integral_one {d : ℕ} {ρ g : Vec d → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hρ_nonneg : ∀ (x : Vec d), 0 ≤ ρ x) (hρ_int : MeasureTheory.Integrable ρ MeasureTheory.volume) (hρ_one : ∫ (x : Vec d), ρ x = 1) (hρ_meas : Measurable ρ) (hg_meas : Measurable g) : MeasureTheory.eLpNorm (MeasureTheory.convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm g p MeasureTheory.volume

Convolution with a nonnegative unit-mass kernel is an L^p contraction on Vec d for 1 ≤ p < ∞.

theorem HCPolySupport.young_convolution_nonneg_integral_one_of_aemeasurable {d : ℕ} {ρ g : Vec d → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (hρ_nonneg : ∀ (x : Vec d), 0 ≤ ρ x) (hρ_int : MeasureTheory.Integrable ρ MeasureTheory.volume) (hρ_one : ∫ (x : Vec d), ρ x = 1) (hρ_meas : Measurable ρ) (hg_meas : AEMeasurable g MeasureTheory.volume) : MeasureTheory.eLpNorm (MeasureTheory.convolution ρ g (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm g p MeasureTheory.volume

AEMeasurable version of young_convolution_nonneg_integral_one, obtained by passing to a measurable representative of the input function.