Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Additivity.CrossTerm

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

AdditivityCrossTerm

Averaged additivity-cross estimates.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_cubeAverage_childAdditivityCrossDensity_le_sqrt_diff_avg_mul_sqrt_sum_avg {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) : |cubeAverage R (childAdditivityCrossDensityOnFamilyOnCube a Q R p q)| ≤ √(cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q)) * √(cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q))

One-child additivity-cross Cauchy estimate with local obligations discharged.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_topHalfEnergyOnFamily_eq_childAdditivityCross_add_responseJOnChild {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) (hCoeff : (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) (hCross_int : MeasureTheory.IntegrableOn (childAdditivityCrossDensityOnFamilyOnCube a Q R p q) (cubeSet R) MeasureTheory.volume) : cubeAverage R (topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q) = cubeAverage R (childAdditivityCrossDensityOnFamilyOnCube a Q R p q) + Ch02.responseJ (Ch02.cubeDomain R) (a.coeffOn R) p q

Child-energy replacement with the concrete additivity-cross density.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.finset_average_sqrt_mul_sqrt_le_sqrt_average_mul_sqrt_average {ι : Type u_1} (S : Finset ι) (hS : S.Nonempty) (A B : ι → ℝ) (hA : ∀ (i : ι), 0 ≤ A i) (hB : ∀ (i : ι), 0 ≤ B i) : (↑S.card)⁻¹ * ∑ i ∈ S, √(A i) * √(B i) ≤ √((↑S.card)⁻¹ * ∑ i ∈ S, A i) * √((↑S.card)⁻¹ * ∑ i ∈ S, B i)

Averaged finite Cauchy for nonnegative scalar data.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_finset_average_le_const_mul_sqrt_average_mul_sqrt_average_of_abs_le {ι : Type u_1} (S : Finset ι) (hS : S.Nonempty) {C : ℝ} (A B X : ι → ℝ) (hC : 0 ≤ C) (hA : ∀ (i : ι), 0 ≤ A i) (hB : ∀ (i : ι), 0 ≤ B i) (hX : ∀ (i : ι), |X i| ≤ C * (√(A i) * √(B i))) : |(↑S.card)⁻¹ * ∑ i ∈ S, X i| ≤ C * (√((↑S.card)⁻¹ * ∑ i ∈ S, A i) * √((↑S.card)⁻¹ * ∑ i ∈ S, B i))

Finite averaged Cauchy after a pointwise absolute-value estimate.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJOnCube_le_childResponseJAverageOnFamilyAtDepth {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : Ch02.responseJ (Ch02.cubeDomain Q) (a.coeffOn Q) p q ≤ childResponseJAverageOnFamilyAtDepth a Q j p q

Descendant response subadditivity for the raw scalar response.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.childResponseJAverageOnFamilyAtDepth_nonneg {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : 0 ≤ childResponseJAverageOnFamilyAtDepth a Q j p q

Child-response averages are nonnegative.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_additivityDiffHalfEnergyDensityOnFamilyOnCube_nonneg {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) : 0 ≤ cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q)

The cube average of the difference half-energy density is nonnegative.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_additivitySumHalfEnergyDensityOnFamilyOnCube_nonneg {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) : 0 ≤ cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q)

The cube average of the sum half-energy density is nonnegative.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivitySumHalfEnergyDensityOnFamilyOnCube_le_two_topHalfEnergy_add_two_childHalfEnergy {d : ℕ} {lam Lam : ℝ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q x : Vec d) (hEll : IsEllipticMatrix lam Lam ((a.coeffOn R).toCoeffField x)) (hCoeff : (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) : additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q x ≤ 2 * topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q x + 2 * topHalfEnergyDensityOnCube R (a.coeffOn R) p q x

Pointwise comparison of the additivity sum energy with parent and child half-energies on one child cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_halfEnergy_le_parentAndChildResponse {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) (hCoeff : (a.coeffOn Q).toCoeffField = (a.coeffOn R).toCoeffField) : cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q) ≤ 2 * cubeAverage R (topHalfEnergyDensityOnCube Q (a.coeffOn Q) p q) + 2 * Ch02.responseJ (Ch02.cubeDomain R) (a.coeffOn R) p q

One-cube averaged comparison of sum energy with parent top energy plus child response.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantsAverage_topHalfEnergy_eq_responseJ {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (j : ℕ) (p q : Vec d) : (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (topHalfEnergyDensityOnCube Q a p q)) = Ch02.responseJ (Ch02.cubeDomain Q) a p q

The descendant average of parent top half-energy over children is the parent response.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantAverage_energy_le_parentAndChildResponse {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube F Q R p q)) ≤ 2 * Ch02.responseJ (Ch02.cubeDomain Q) (F.coeffOn Q) p q + 2 * childResponseJAverageOnFamilyAtDepth F Q j p q

The descendant-averaged sum-energy factor is controlled by twice the parent response plus twice the child-response average.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantsAverage_additivitySumHalfEnergyOnDependentFamily_le_four_childResponse {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; (descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube F Q R p q)) ≤ 4 * childResponseJAverageOnFamilyAtDepth F Q j p q

The descendant-averaged sum-energy factor is bounded by four times the child-response average.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.sqrt_le_two_mul_sqrt_of_le_four_mul {x y : ℝ} (hxy : x ≤ 4 * y) : √x ≤ 2 * √y

Square-root form of a 4-multiple upper bound.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_productChildCrossDensity_le_constant_mul_sqrtDifferenceMean_mul_sqrtSumMean {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (φ : Vec d → ℝ) (p q : Vec d) {C : ℝ} (hCut : |1 - cubeAverage R φ| ≤ C) : |(1 - cubeAverage R φ) * cubeAverage R (childAdditivityCrossDensityOnFamilyOnCube a Q R p q)| ≤ C * (√(cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q)) * √(cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q)))

One-child additivity-cross estimate with the cutoff mean factor included.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_additivityCross_le_constant_mul_sqrtDiffEnergy_mul_sqrtSumEnergy {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q : Vec d) {C : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) : |concreteAdditivityCrossTermOnFamilyAtDepth a Q j φ p q| ≤ C * (√(descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q)) * √(descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q)))

Descendant-averaged additivity-cross term after the one-cube Cauchy step.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_additivityCross_le_twoConstant_mul_sqrtDiffEnergy_mul_sqrtResponseMean {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q : Vec d) {C : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; |concreteAdditivityCrossTermOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(descendantsAverage Q j fun (R : TriadicCube d) => cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube F Q R p q)) * √(childResponseJAverageOnFamilyAtDepth F Q j p q))

Deterministic additivity-cross bound for the Chapter 4 dependent family, with the second energy factor reduced to child responses.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_additivityCross_le_constant_mul_sqrtPartitionDefect_mul_sqrtChildResponse {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q : Vec d) {C : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; |concreteAdditivityCrossTermOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(responseJPartitionDefectOnFamilyAtDepth F Q j p q) * √(childResponseJAverageOnFamilyAtDepth F Q j p q))

Deterministic additivity-cross bound in the manuscript form, with the difference-energy factor identified as the response partition defect.