Coarse-graining support:

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

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

AdditivityDensities

Additivity-cross densities and pointwise elliptic estimates.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.half_quad_eq_additivity_cross_add_half_quad {d : ℕ} (A : Mat d) (top child : Vec d) : 1 / 2 * vecDot top (matVecMul (symmPart A) top) = 1 / 2 * vecDot (top - child) (matVecMul (symmPart A) (top - child)) + vecDot (top - child) (matVecMul (symmPart A) child) + 1 / 2 * vecDot child (matVecMul (symmPart A) child)

Quadratic algebra behind the child additivity-cross term.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.childAdditivityCrossDensityOnFamilyOnCube {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) : Vec d → ℝ

Concrete child-cube cross density for a deterministic coefficient family.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.concreteAdditivityCrossTermOnFamilyAtDepth {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (p q : Vec d) : ℝ

Concrete additivity-cross term over all depth-j children.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.childResponseJAverageOnFamilyAtDepth {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : ℝ

Unweighted average of child responses for a deterministic triadic coefficient family.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJPartitionDefectOnFamilyAtDepth {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) (j : ℕ) (p q : Vec d) : ℝ

Deterministic child-minus-parent response defect for a triadic coefficient family.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) : Vec d → ℝ

The local half-energy of the top-minus-child gradient difference on one child cube.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivitySumHalfEnergyDensityOnFamilyOnCube {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) : Vec d → ℝ

The local half-energy of the top-plus-child gradient sum on one child cube.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.childAdditivityCrossDensityOnFamilyOnCube_integrableOn {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) : MeasureTheory.IntegrableOn (childAdditivityCrossDensityOnFamilyOnCube a Q R p q) (cubeSet R) MeasureTheory.volume

The concrete child additivity-cross density is locally integrable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.childAdditivityCrossDensityOnFamilyOnCube_eq_half_diff_dot_symmPart_sum {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q x : Vec d) : childAdditivityCrossDensityOnFamilyOnCube a Q R p q x = 1 / 2 * vecDot (canonicalMaximizerGradientOnCube Q (a.coeffOn Q) p q x - canonicalMaximizerGradientOnCube R (a.coeffOn R) p q x) (matVecMul (symmPart ((a.coeffOn R).toCoeffField x)) (canonicalMaximizerGradientOnCube Q (a.coeffOn Q) p q x + canonicalMaximizerGradientOnCube R (a.coeffOn R) p q x))

The concrete child additivity-cross density is the manuscript 1/2 (top-child) · a_s (top+child) density.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_half_vecDot_matVecMul_symmPart_le_sqrt_half_quad_mul_sqrt_half_quad_of_isEllipticMatrix {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) (ξ η : Vec d) : |1 / 2 * vecDot ξ (matVecMul (symmPart A) η)| ≤ √(1 / 2 * vecDot ξ (matVecMul (symmPart A) ξ)) * √(1 / 2 * vecDot η (matVecMul (symmPart A) η))

Pointwise Cauchy for the symmetric coefficient energy.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_childAdditivityCrossDensityOnFamilyOnCube_le_sqrt_diff_mul_sqrt_sum_of_isEllipticMatrix {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)) : |childAdditivityCrossDensityOnFamilyOnCube a Q R p q x| ≤ √(additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q x) * √(additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q x)

Pointwise local Cauchy estimate for the concrete child additivity-cross density.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube_nonneg_of_isEllipticMatrix {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)) : 0 ≤ additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q x

The local difference half-energy density is nonnegative at elliptic points.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivitySumHalfEnergyDensityOnFamilyOnCube_nonneg_of_isEllipticMatrix {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)) : 0 ≤ additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q x

The local sum half-energy density is nonnegative at elliptic points.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivityDiffHalfEnergyDensityOnFamilyOnCube_integrableOn {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) : MeasureTheory.IntegrableOn (additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q) (cubeSet R) MeasureTheory.volume

The local difference half-energy density is locally integrable.

Difference energy and the response partition defect

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cubeAverage_additivityEnergyDensity_eq_responseJ_sub_responseValue {d : ℕ} (a : Ch02.TriadicCoeffFamily d) (Q R : TriadicCube d) (p q : Vec d) (w : Ch02.Solution (Ch02.cubeDomain R) (a.coeffOn R)) (hgrad : w.toH1.grad = canonicalMaximizerGradientOnCube Q (a.coeffOn Q) p q) : cubeAverage R (additivityDiffHalfEnergyDensityOnFamilyOnCube a Q R p q) = Ch02.responseJ (Ch02.cubeDomain R) (a.coeffOn R) p q - Ch02.responseValue (Ch02.cubeDomain R) (a.coeffOn R) p q w

One-cube second variation in the concrete Section 5.3 notation. If a child cube solution has the parent gradient, then the local difference half-energy is the gap between the child canonical response and that solution's response value.

@[simp]

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.h1Function_restrict_grad {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVopen : IsOpen V) (hVU : V ⊆ U) : (u.restrict hVopen hVU).grad = u.grad