Coarse-graining support: Support.Sobolev.Foundations.PoincareLpKernel.TimeCollapse

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

Time-collapse estimates for the Riesz-kernel Poincare integrand

Collects the intervalIntegral-level lemmas that bound the time-averaged segment-blend integrand against rieszKernel.

theorem HCPolySupport.intervalIntegral_inv_pow_if_norm_sub_le_mul_le_rieszKernel {d : ℕ} [NeZero d] {x z : Vec d} {R : ℝ} (hR : 0 < R) : (∫ (t : ℝ) in 0..1, ((1 - t) ^ (d + 1))⁻¹ * if ‖x - z‖ ≤ (1 - t) * R then ‖x - z‖ else 0) ≤ R ^ d / ↑d * rieszKernel x z

theorem HCPolySupport.setIntegral_inv_pow_setIntegral_inter_closedBall_le_rieszKernel {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {R : ℝ} (hR : 0 < R) {φ : Vec d → ℝ} (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) (hφ_meas : AEMeasurable φ (MeasureTheory.volume.restrict U)) (hφK_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * rieszKernel x z) U MeasureTheory.volume) : ∫ (t : ℝ) in Set.Ioc 0 1, ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * R), φ z * ‖x - z‖ ≤ R ^ d / ↑d * ∫ (z : Vec d) in U, φ z * rieszKernel x z

theorem HCPolySupport.intervalIntegrable_inv_pow_setIntegral_inter_closedBall {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {R : ℝ} (hR : 0 < R) {φ : Vec d → ℝ} (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) (hφ_meas : AEMeasurable φ (MeasureTheory.volume.restrict U)) (hφK_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * rieszKernel x z) U MeasureTheory.volume) : IntervalIntegrable (fun (t : ℝ) => ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * R), φ z * ‖x - z‖) MeasureTheory.volume 0 1

theorem HCPolySupport.intervalIntegral_inv_pow_setIntegral_inter_closedBall_le_rieszKernel {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {R : ℝ} (hR : 0 < R) {φ : Vec d → ℝ} (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) (hφ_meas : AEMeasurable φ (MeasureTheory.volume.restrict U)) (hφK_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * rieszKernel x z) U MeasureTheory.volume) : ∫ (t : ℝ) in 0..1, ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * R), φ z * ‖x - z‖ ≤ R ^ d / ↑d * ∫ (z : Vec d) in U, φ z * rieszKernel x z