Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaIntegration

Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaIntegration #

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

Integration of an untruncated weighted good-lambda inequality #

This module closes the natural one-level estimate under the untruncated measures nu_f = ‖f‖^2 dmu and nu_g = ‖g‖^2 dmu. The self term is integrated only up to a finite level R. The substitution t = 2 M s produces the smaller cutoff R / (2 M), which is bounded by R when 1 / 2 < M. Reabsorption is therefore legitimate at every finite cutoff, and monotone convergence then removes the cutoff without assuming f is in L^p.

source
theorem HCPolySupport.CubeCalderonZygmund.low_weighted_layercake_le {alpha : Type u_1} [MeasurableSpace alpha] (nu : MeasureTheory.Measure alpha) {u : alpha → ℝ} {p M lambda0 : ℝ} (hp : 2 < p) (hlambda0 : 0 ≤ lambda0) :
ENNReal.ofReal (p - 2) * ∫⁻ (t : ℝ) in Set.Ioo 0 lambda0, nu {x : alpha | M * t < u x} * ENNReal.ofReal (t ^ (p - 3)) ≤ nu Set.univ * ENNReal.ofReal (lambda0 ^ (p - 2))

The low-level portion of a weighted layer-cake integral is controlled by the total weighted mass.

source
noncomputable def HCPolySupport.CubeCalderonZygmund.cutoffTailMoment {alpha : Type u_1} [MeasurableSpace alpha] (nu : MeasureTheory.Measure alpha) (u : alpha → ℝ) (p a R : ℝ) :
ENNReal

The finite layer-cutoff integral used in the reabsorption argument.

Equations
Instances For
    source
    theorem HCPolySupport.CubeCalderonZygmund.lp_le_of_oneLevel_weighted_tail {alpha : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace alpha] [NormedAddCommGroup E] [NormedAddCommGroup F] {mu : MeasureTheory.Measure alpha} {f : alpha → E} {g : alpha → F} {p M eps lambda0 : ℝ} {theta B : ENNReal} (hf : MeasureTheory.AEStronglyMeasurable f mu) (hg : MeasureTheory.AEStronglyMeasurable g mu) (hp : 2 < p) (hM : 0 < M) (hhalfM : 1 / 2 < M) (heps : 0 < eps) (hlambda0 : 0 < lambda0) (hnuf : (sqWeightedMeasure f mu) Set.univ ≠ ⊤) (hB : B ≠ ⊤) (hdata : ∫⁻ (x : alpha), ENNReal.ofReal (‖g x‖ ^ p / (eps / 2) ^ (p - 2)) ∂mu ≠ ⊤) (hsmall : theta * ENNReal.ofReal ((2 * M) ^ (p - 2)) < 1) (h_tail : ∀ (t : ℝ), lambda0 ≤ t → (sqWeightedMeasure f mu) {x : alpha | M * t < ‖f x‖} ≤ theta * (sqWeightedMeasure f mu) {x : alpha | t / 2 < ‖f x‖} + B * (sqWeightedMeasure g mu) {x : alpha | eps * t / 2 < ‖g x‖}) :
    ∫⁻ (x : alpha), ENNReal.ofReal (‖f x‖ ^ p / M ^ (p - 2)) ∂mu ≤ ((sqWeightedMeasure f mu) Set.univ * ENNReal.ofReal (lambda0 ^ (p - 2)) + B * ∫⁻ (x : alpha), ENNReal.ofReal (‖g x‖ ^ p / (eps / 2) ^ (p - 2)) ∂mu) / (1 - theta * ENNReal.ofReal ((2 * M) ^ (p - 2)))

    Integrate and reabsorb the natural untruncated weighted good-lambda estimate.

    The only finiteness assumptions used before the conclusion are the finite square-weighted mass of f, the finite displayed data moment, and the finiteness of the scalar coefficient B. In particular, there is no L^p hypothesis on f.