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

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

noncomputable def HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] (f : α → E) (μ : MeasureTheory.Measure α) : MeasureTheory.Measure α

The measure ‖f‖² dμ used to weight the layer-cake argument.

Equations

• HCPolySupport.CubeCalderonZygmund.sqWeightedMeasure f μ = μ.withDensity fun (x : α) => ENNReal.ofReal (‖f x‖ ^ 2)

def HCPolySupport.CubeCalderonZygmund.truncNorm {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : α → E) (m : ℝ) : α → ℝ

The pointwise truncation ‖f‖ ∧ m appearing in the Caffarelli--Peral proof.

Equations

• HCPolySupport.CubeCalderonZygmund.truncNorm f m x = min ‖f x‖ m

theorem HCPolySupport.CubeCalderonZygmund.lintegral_truncNorm_div_rpow_eq_weighted_layercake {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p a m : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hp : 2 < p) (ha : 0 < a) (hm : 0 ≤ m) : ∫⁻ (x : α), ENNReal.ofReal ((truncNorm f m x / a) ^ (p - 2)) ∂sqWeightedMeasure f μ = ENNReal.ofReal (p - 2) * ∫⁻ (t : ℝ) in Set.Ioi 0, (sqWeightedMeasure f μ) {x : α | a * t < truncNorm f m x} * ENNReal.ofReal (t ^ (p - 3))

Layer cake under the squared-density measure, with the threshold written in the source form a * λ. This is an ENNReal identity and therefore needs no integrability assumption.

theorem HCPolySupport.CubeCalderonZygmund.truncNorm_rpow_div_eq_div_rpow_mul_sq {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (f : α → E) {p a m : ℝ} (hp : 2 < p) (ha : 0 < a) (hm : 0 ≤ m) (x : α) : truncNorm f m x ^ p / a ^ (p - 2) = (truncNorm f m x / a) ^ (p - 2) * truncNorm f m x ^ 2

The algebraic normalization which turns the truncated Lᵖ power into the weighted power used by layer cake.

theorem HCPolySupport.CubeCalderonZygmund.lintegral_truncNorm_rpow_div_le_weighted_layercake {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} {p a m : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hp : 2 < p) (ha : 0 < a) (hm : 0 ≤ m) : ∫⁻ (x : α), ENNReal.ofReal (truncNorm f m x ^ p / a ^ (p - 2)) ∂μ ≤ ENNReal.ofReal (p - 2) * ∫⁻ (t : ℝ) in Set.Ioi 0, (sqWeightedMeasure f μ) {x : α | a * t < truncNorm f m x} * ENNReal.ofReal (t ^ (p - 3))

The finite-truncation estimate used for f_m in the source proof. It turns the truncated Lᵖ power into the weighted layer-cake integral, retaining the exact threshold a * t.