Coarse-graining support: Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.EnergyDensities

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

EnergyDensities

Energy densities, product densities, and integrability facts.

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

Parent half-energy density 1/2 ∇v · a∇v.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredResponseJOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : ℝ

Centered raw Ch2 response on a cube.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredProductDensityOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : Vec d → ℝ

The product density in the centered splitting.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredGradientLinearDensityOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : Vec d → ℝ

The q0 linear density in the centered splitting.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredFluxLinearDensityOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : Vec d → ℝ

The p0 linear density in the centered splitting.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductTermOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : ℝ

The cutoff product term in the deterministic centered split.

Equations

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

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

The cutoff oscillation term in the deterministic centered split.

Equations

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

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

The mean-defect parent-energy term before child-energy replacement.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivityCrossTermOnCubeAtDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) (φ : Vec d → ℝ) (cross : TriadicCube d → ℝ) : ℝ

Scalar additivity-cross term, indexed by child cubes.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffGradientLinearTermOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : ℝ

The cutoff q0 linear term.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffFluxLinearTermOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : ℝ

The cutoff p0 linear term.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffLinearPairTermOnCube {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) : ℝ

The two cutoff linear terms, in manuscript order.

Equations

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

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

Cutoff-weighted child response for a deterministic triadic coefficient family.

Equations

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

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centered_product_add_linear_terms_eq_half_vecDot_sub_half_vecDot {d : ℕ} (g f p0 q0 : Vec d) : 1 / 2 * vecDot (g - p0) (f - q0) + 1 / 2 * vecDot q0 (g - p0) + 1 / 2 * vecDot p0 (f - q0) = 1 / 2 * vecDot g f - 1 / 2 * vecDot p0 q0

Pure vector algebra behind the product plus two linear terms.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredProduct_add_linear_densities_eq_topHalfEnergy_sub_half_dot {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 x : Vec d) : centeredProductDensityOnCube Q a p q p0 q0 x + centeredGradientLinearDensityOnCube Q a p q p0 q0 x + centeredFluxLinearDensityOnCube Q a p q p0 q0 x = topHalfEnergyDensityOnCube Q a p q x - 1 / 2 * vecDot p0 q0

Pointwise algebra turning the parent energy into product plus linear terms.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredResponseJOnCube_eq_cubeAverage_topHalfEnergy_sub_half_dot {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : centeredResponseJOnCube Q a p q p0 q0 = cubeAverage Q (topHalfEnergyDensityOnCube Q a p q) - 1 / 2 * vecDot p0 q0

Raw response as a parent half-energy average, centered by p0 · q0 / 2.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJOnCube_eq_cubeAverage_topHalfEnergy {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q : Vec d) : Ch02.responseJ (Ch02.cubeDomain Q) a p q = cubeAverage Q (topHalfEnergyDensityOnCube Q a p q)

Raw response as a parent half-energy average.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.ch02_variationEnergyIntegrand_integrableOn {d : ℕ} (U : Ch02.Domain d) (a : Ch02.CoeffOn U) (v : Ch02.Solution U a) : MeasureTheory.IntegrableOn (Ch02.variationEnergyIntegrand U a v) U.carrier MeasureTheory.volume

The Chapter 2 energy integrand of a public solution is locally integrable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.ch02_responseIntegrand_integrableOn {d : ℕ} (U : Ch02.Domain d) (a : Ch02.CoeffOn U) (p q : Vec d) (v : Ch02.Solution U a) : MeasureTheory.IntegrableOn (Ch02.responseIntegrand U a p q v) U.carrier MeasureTheory.volume

The Chapter 2 response integrand of a public solution is locally integrable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.topHalfEnergyDensityOnCube_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q : Vec d) : MeasureTheory.IntegrableOn (topHalfEnergyDensityOnCube Q a p q) (cubeSet Q) MeasureTheory.volume

The parent half-energy density is integrable on the half-open cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.topHalfEnergyDensityOnCube_ae_nonneg_cubeSet {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q : Vec d) : 0 ≤ᵐ[volumeMeasureOn (cubeSet Q)] topHalfEnergyDensityOnCube Q a p q

The parent half-energy density is nonnegative a.e. on the half-open cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integrableOn_mul_left_of_integrableOn_of_ae_bounded {d : ℕ} {U : Set (Vec d)} {φ f : Vec d → ℝ} {C : ℝ} (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hφ_meas : MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn U)) (hφ_bound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, ‖φ x‖ ≤ C) : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * f x) U MeasureTheory.volume

A bounded a.e.-strongly-measurable multiplier preserves local integrability.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube_component_integrableOn {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 : Vec d) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => canonicalMaximizerGradientDefectOnCube Q a p q p0 x i) (cubeSet Q) MeasureTheory.volume

Components of the raw canonical maximizer gradient defect are integrable on the parent cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube_component_integrableOn {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q q0 : Vec d) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => canonicalMaximizerFluxDefectOnCube Q a p q q0 x i) (cubeSet Q) MeasureTheory.volume

Components of the raw canonical maximizer flux defect are integrable on the parent cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredProductDensityOnCube_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : MeasureTheory.IntegrableOn (centeredProductDensityOnCube Q a p q p0 q0) (cubeSet Q) MeasureTheory.volume

The centered product density in the deterministic Section 5.3 split is integrable on the parent cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredGradientLinearDensityOnCube_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : MeasureTheory.IntegrableOn (centeredGradientLinearDensityOnCube Q a p q p0 q0) (cubeSet Q) MeasureTheory.volume

The centered gradient-linear density in the deterministic Section 5.3 split is integrable on the parent cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.centeredFluxLinearDensityOnCube_integrableOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (p q p0 q0 : Vec d) : MeasureTheory.IntegrableOn (centeredFluxLinearDensityOnCube Q a p q p0 q0) (cubeSet Q) MeasureTheory.volume

The centered flux-linear density in the deterministic Section 5.3 split is integrable on the parent cube.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffOscillationTermOnCubeAtDepth_integrableOn_descendants_of_ae_bounded {d : ℕ} (Q : TriadicCube d) (a : Ch02.CoeffOn (Ch02.cubeDomain Q)) (j : ℕ) {φ : Vec d → ℝ} {C : ℝ} (p q : Vec d) (hφ_meas : MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn (cubeSet Q))) (hφ_bound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet Q), ‖φ x‖ ≤ C) (R : TriadicCube d) : R ∈ descendantsAtDepth Q j → MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q a p q x) (cubeSet R) MeasureTheory.volume

A bounded cutoff gives the descendant cutoff-oscillation integrability condition.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_cubeAverage_mul_nonneg_le_mul_cubeAverage_of_ae_abs_le {d : ℕ} (R : TriadicCube d) {w f : Vec d → ℝ} {B : ℝ} (hf_int : MeasureTheory.IntegrableOn f (cubeSet R) MeasureTheory.volume) (hwf_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => w x * f x) (cubeSet R) MeasureTheory.volume) (hf_nonneg : 0 ≤ᵐ[volumeMeasureOn (cubeSet R)] f) (hw_bound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet R), |w x| ≤ B) : |cubeAverage R fun (x : Vec d) => w x * f x| ≤ B * cubeAverage R f

Cube-average estimate for a bounded oscillating scalar times a nonnegative integrable density.