Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.LocalWeightedTailRestrict

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

Local weighted comparison tails

This is the restriction-stable form of the weighted comparison estimate. It requires measurability only on the ball (or other local set) under study.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_tail_le_comparison_restrict {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {B : Set α} (hB : MeasurableSet B) {f v : α → E} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict B)) (hv : MeasureTheory.AEStronglyMeasurable v (μ.restrict B)) {r a : ℝ} (hr : 2 < r) (ha : 0 < a) : (sqWeightedMeasure f μ) ({x : α | a < ‖f x‖} ∩ B) ≤ 2 * ENNReal.ofReal ((a / 2) ^ (2 - r)) * ∫⁻ (x : α) in B, ENNReal.ofReal (‖v x‖ ^ r) ∂μ + 6 * ∫⁻ (x : α) in B, ENNReal.ofReal (‖f x - v x‖ ^ 2) ∂μ

The weighted comparison-tail estimate with all measurability assumptions localized to the measurable set B.