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

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

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_apply₀ {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} (f : α → E) {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : (sqWeightedMeasure f μ) s = ∫⁻ (x : α) in s, ENNReal.ofReal (‖f x‖ ^ 2) ∂μ

The defining density of sqWeightedMeasure, on sets measurable up to a μ-null set.

theorem HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure_tail_le_comparison {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {B : Set α} (hB : MeasurableSet B) {f v : α → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hv : MeasureTheory.AEStronglyMeasurable v μ) {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) ∂μ