High-contrast homogenization: Provider.Response.MeanDefect

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The mean-defect term of the cutoff-energy estimate

The mean-defect term compares the cutoff's childwise means against the childwise averages of the parent energy density. Replacing the parent gradient by the child gradient on each child splits it into two pieces: the cutoff-weighted child responses, and a cross term built from the gradient difference.

The cross term is quadratic in the gradient difference and linear in the child gradient, so the Cauchy-Schwarz inequality in the symmetric metric, applied first on each child and then across the children, bounds it by the geometric mean of the childwise difference energy and the childwise sum energy. The sum energy is at most twice the parent energy plus twice the child responses, which gives the closed bound recorded below.

Nothing here is an inequality between annealed quantities: the cutoff-weighted child responses are kept as an explicit term, because they cancel only after averaging over a stationary law, where the child responses become independent of the child's position.

Elementary facts about descendant averages and cube averages

theorem HCPolySupport.HighContrast.Response.descendantsAverage_const_mul {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => c * F R) = c * descendantsAverage Q j F

Descendant averages commute with scalar multiples.

theorem HCPolySupport.HighContrast.Response.descendantsAverage_mono {d : ℕ} (Q : TriadicCube d) (j : ℕ) {F G : TriadicCube d → ℝ} (h : ∀ R ∈ descendantsAtDepth Q j, F R ≤ G R) : descendantsAverage Q j F ≤ descendantsAverage Q j G

Descendant averages are monotone.

theorem HCPolySupport.HighContrast.Response.cubeAverage_le_of_le {d : ℕ} (R : TriadicCube d) {f : Vec d → ℝ} {B : ℝ} (hint : MeasureTheory.IntegrableOn f (cubeSet R) MeasureTheory.volume) (hB : ∀ (x : Vec d), f x ≤ B) : cubeAverage R f ≤ B

A pointwise two-sided bound passes to the cube average.

theorem HCPolySupport.HighContrast.Response.le_cubeAverage_of_le {d : ℕ} (R : TriadicCube d) {f : Vec d → ℝ} {B : ℝ} (hint : MeasureTheory.IntegrableOn f (cubeSet R) MeasureTheory.volume) (hB : ∀ (x : Vec d), B ≤ f x) : B ≤ cubeAverage R f

A pointwise lower bound passes to the cube average.

theorem HCPolySupport.HighContrast.Response.abs_one_sub_cubeAverage_le_one {d : ℕ} (R : TriadicCube d) {φ : Vec d → ℝ} (hint : MeasureTheory.IntegrableOn φ (cubeSet R) MeasureTheory.volume) (h0 : ∀ (x : Vec d), 0 ≤ φ x) (h2 : ∀ (x : Vec d), φ x ≤ 2) : |1 - cubeAverage R φ| ≤ 1

The childwise weights of a cutoff bounded between zero and two are bounded by one in absolute value.

The split of the mean-defect term

theorem HCPolySupport.HighContrast.Response.meanDefectTopEnergyTermOnCubeAtDepth_eq_cross_add_cutoffWeightedChild {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p r : Vec d) (hCoeff : ∀ R ∈ descendantsAtDepth Q j, (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) : Book.Ch05.Section53.JUpperBoundWeakNorms.meanDefectTopEnergyTermOnCubeAtDepth Q (a.coeffOn Q) j φ p r = Book.Ch05.Section53.JUpperBoundWeakNorms.concreteAdditivityCrossTermOnFamilyAtDepth a Q j φ p r + Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffWeightedChildResponseJOnFamilyAtDepth a Q j φ p r

The mean-defect term splits into the cutoff-weighted child responses and the additivity cross term.

The cross-term bound

theorem HCPolySupport.HighContrast.Response.descendantsAverage_additivitySumHalfEnergy_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p r : Vec d) (hCoeff : ∀ R ∈ descendantsAtDepth Q j, (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (Book.Ch05.Section53.JUpperBoundWeakNorms.additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p r)) ≤ 4 * Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) (a.coeffOn Q) p r + 2 * Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth a Q j p r

The childwise sum energies average to at most four times the parent response plus twice the partition defect.

theorem HCPolySupport.HighContrast.Response.abs_concreteAdditivityCrossTermOnFamilyAtDepth_le_sqrt_mul_sqrt {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p r : Vec d) (hCoeff : ∀ R ∈ descendantsAtDepth Q j, (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) (hweight : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ 1) : |Book.Ch05.Section53.JUpperBoundWeakNorms.concreteAdditivityCrossTermOnFamilyAtDepth a Q j φ p r| ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p r)) * √(4 * Book.Ch02.responseJ (Book.Ch02.cubeDomain Q) (a.coeffOn Q) p r + 2 * Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth a Q j p r)

The cross term is bounded by the geometric mean of the childwise difference energy and the closed sum-energy majorant.

The shape of the bound

theorem HCPolySupport.HighContrast.Response.sqrt_mul_sqrt_four_add_two_le {X J T : ℝ} (hJ : 0 ≤ J) (hT : 0 ≤ T) : √X * √(4 * J + 2 * T) ≤ 2 * (√X * √J) + √2 * (√X * √T)

The closed bound in the shape used by the localization argument.

theorem HCPolySupport.HighContrast.Response.sqrt_mul_sqrt_four_add_two_le_two_mul_add_four_mul {T J : ℝ} (hJ : 0 ≤ J) (hT : 0 ≤ T) : √T * √(4 * J + 2 * T) ≤ 2 * T + 4 * (√T * √J)

The closed bound is at most the coarser shape with the two separated coefficients.

The discharged cutoff-energy estimate

theorem HCPolySupport.HighContrast.Response.integrableOn_adaptedPreYoungCutoff_pullback {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (R : TriadicCube d) : MeasureTheory.IntegrableOn (fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) (cubeSet R) MeasureTheory.volume

The pulled-back adapted cutoff is integrable on every triadic cube.

theorem HCPolySupport.HighContrast.Response.abs_one_sub_cubeAverage_adaptedPreYoungCutoff_le_one {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (R : TriadicCube d) : |1 - cubeAverage R fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)| ≤ 1

The adapted cutoff's childwise weights are bounded by one.