Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.DeterministicAssembly

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

DeterministicAssembly

Deterministic manuscript pointwise assembly.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_responseJDifference_le_additivityError_cutoffOscillation_pair_productRHS {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (s : ℝ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (dualField cutoffGradient : Vec d → Vec d) {C cutoffCircOne cutoffCircS cutoffDerivative poincareConst cutoffConstant centeredCutoffConstant : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hOsc_int : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet R) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet Q) (hcutoffGradient_eq : cutoffGradient = scalarCutoffGradientField φ) (hcutoffDerivative : 0 ≤ cutoffDerivative) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hdualField : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => dualField x i) 2 (normalizedCubeMeasure Q)) (hcutoffGradient : MeasureTheory.MemLp cutoffGradient ⊤ (normalizedCubeMeasure Q)) (hcutoffConstant : 0 ≤ cutoffConstant) (hcenteredCutoffConstant : 0 ≤ centeredCutoffConstant) (hpoincareConst : 0 ≤ poincareConst) (hcutoffCircOne : 0 ≤ cutoffCircOne) (hcutoffCircS : 0 ≤ cutoffCircS) (hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q poincareConst (cubeFluctuation Q (canonicalMaximizerPotentialDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0)) dualField N) (hcutoffSmooth : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => cutoffGradient x i) (hcutoffDeriv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => cutoffGradient x i) z‖ ≤ cutoffDerivative) (hdualCircOne : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => dualField x i) ≤ cutoffCircOne) (hdualCircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => dualField x i) ≤ cutoffCircS) (hcutoffConstant_bound : cubeLpNorm Q 2 (canonicalMaximizerPotentialDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0) * (cutoffDerivative + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ cutoffGradient) ≤ cutoffConstant) (hcenteredCutoffConstant_bound : 2 * (cubeScaleFactor Q * cutoffDerivative * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * (↑(Fintype.card (Fin d)) * poincareConst) * 3 ^ (↑d + 1) * cutoffCircOne)) + cubeLpNorm Q ⊤ cutoffGradient * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * poincareConst) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cutoffCircS))) ≤ centeredCutoffConstant) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; |centeredResponseJOnCube Q (F.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(responseJPartitionDefectOnFamilyAtDepth F Q j p q) * √(childResponseJAverageOnFamilyAtDepth F Q j p q)) + |cutoffOscillationTermOnCubeAtDepth Q (F.coeffOn Q) j φ p q| + |cutoffLinearPairTermOnCube Q (F.coeffOn Q) φ p q p0 q0| + cutoffProductBridgeRHS Q s cutoffGradient (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q 1 p q q0 a.toFun) (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun) ‖Ch04.canonicalScalarResponseFluxAverageCubeSet Q Q p q a.toFun - q0‖ cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant

Deterministic assembled Section 5.3 estimate with the actual product term replaced by the scalar-response weak-norm cutoff-product bridge. The cutoff-oscillation and linear-pair terms are still displayed separately here; those are the next deterministic terms to insert before taking expectations.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_responseJDifference_le_additivityError_cutoffBound_pair_productRHS {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (s : ℝ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (dualField cutoffGradient : Vec d → Vec d) {C B Cosc scaleSep cutoffCircOne cutoffCircS cutoffDerivative poincareConst cutoffConstant centeredCutoffConstant : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) (hφ_meas : MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn (cubeSet Q))) (hφ_bound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet Q), ‖φ x‖ ≤ B) (hOscPoint : ∀ R ∈ descendantsAtDepth Q j, ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet R), |cubeAverage R φ - φ x| ≤ Cosc * scaleSep) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet Q) (hcutoffGradient_eq : cutoffGradient = scalarCutoffGradientField φ) (hcutoffDerivative : 0 ≤ cutoffDerivative) (hs_pos : 0 < s) (hs_lt_one : s < 1) (hdualField : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => dualField x i) 2 (normalizedCubeMeasure Q)) (hcutoffGradient : MeasureTheory.MemLp cutoffGradient ⊤ (normalizedCubeMeasure Q)) (hcutoffConstant : 0 ≤ cutoffConstant) (hcenteredCutoffConstant : 0 ≤ centeredCutoffConstant) (hpoincareConst : 0 ≤ poincareConst) (hcutoffCircOne : 0 ≤ cutoffCircOne) (hcutoffCircS : 0 ≤ cutoffCircS) (hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q poincareConst (cubeFluctuation Q (canonicalMaximizerPotentialDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0)) dualField N) (hcutoffSmooth : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => cutoffGradient x i) (hcutoffDeriv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => cutoffGradient x i) z‖ ≤ cutoffDerivative) (hdualCircOne : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => dualField x i) ≤ cutoffCircOne) (hdualCircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => dualField x i) ≤ cutoffCircS) (hcutoffConstant_bound : cubeLpNorm Q 2 (canonicalMaximizerPotentialDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0) * (cutoffDerivative + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ cutoffGradient) ≤ cutoffConstant) (hcenteredCutoffConstant_bound : 2 * (cubeScaleFactor Q * cutoffDerivative * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * (↑(Fintype.card (Fin d)) * poincareConst) * 3 ^ (↑d + 1) * cutoffCircOne)) + cubeLpNorm Q ⊤ cutoffGradient * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * poincareConst) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cutoffCircS))) ≤ centeredCutoffConstant) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; |centeredResponseJOnCube Q (F.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(responseJPartitionDefectOnFamilyAtDepth F Q j p q) * √(childResponseJAverageOnFamilyAtDepth F Q j p q)) + Cosc * scaleSep * Ch04.restrictionResponseJObservableCubeSet Q p q a + |cutoffLinearPairTermOnCube Q (F.coeffOn Q) φ p q p0 q0| + cutoffProductBridgeRHS Q s cutoffGradient (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q 1 p q q0 a.toFun) (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun) ‖Ch04.canonicalScalarResponseFluxAverageCubeSet Q Q p q a.toFun - q0‖ cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant

Deterministic assembled Section 5.3 estimate with both the cutoff oscillation term and the product term replaced by their manuscript bounds. The linear pair is the only displayed deterministic split term still not inserted here.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_responseJDifference_le_additivityError_cutoffBound_weakNorms_productRHS {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (s t : ℝ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) (dualField cutoffGradient : Vec d → Vec d) {C B Cosc scaleSep BφS BφT cutoffCircOne cutoffCircS cutoffDerivative poincareConst cutoffConstant centeredCutoffConstant : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradField : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (φ x • canonicalMaximizerGradientDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 x) i) (cubeSet Q) MeasureTheory.volume) (hFluxField : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (φ x • canonicalMaximizerFluxDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q q0 x) i) (cubeSet Q) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) (hφ_meas : MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn (cubeSet Q))) (hφ_bound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet Q), ‖φ x‖ ≤ B) (hOscPoint : ∀ R ∈ descendantsAtDepth Q j, ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet R), |cubeAverage R φ - φ x| ≤ Cosc * scaleSep) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet Q) (hcutoffGradient_eq : cutoffGradient = scalarCutoffGradientField φ) (hcutoffDerivative : 0 ≤ cutoffDerivative) (hs_pos : 0 < s) (hs_lt_one : s < 1) (ht_pos : 0 < t) (hBφS : 0 ≤ BφS) (hBφT : 0 ≤ BφT) (hφDualS : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N φ ≤ BφS) (hφDualT : ∀ (N : ℕ), cubeBesovDualTestNorm Q t 2 1 N φ ≤ BφT) (hφMem : CubeBesovDualLocalMemLpGlobal Q 2 φ) (hdualField : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => dualField x i) 2 (normalizedCubeMeasure Q)) (hcutoffGradient : MeasureTheory.MemLp cutoffGradient ⊤ (normalizedCubeMeasure Q)) (hcutoffConstant : 0 ≤ cutoffConstant) (hcenteredCutoffConstant : 0 ≤ centeredCutoffConstant) (hpoincareConst : 0 ≤ poincareConst) (hcutoffCircOne : 0 ≤ cutoffCircOne) (hcutoffCircS : 0 ≤ cutoffCircS) (hfull : ∀ (N : ℕ), CubeDescendantDualFullVectorPoincareEstimate Q poincareConst (cubeFluctuation Q (canonicalMaximizerPotentialDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0)) dualField N) (hcutoffSmooth : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => cutoffGradient x i) (hcutoffDeriv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => cutoffGradient x i) z‖ ≤ cutoffDerivative) (hdualCircOne : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => dualField x i) ≤ cutoffCircOne) (hdualCircS : ∀ (i : Fin d) (N : ℕ), (cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => dualField x i) ≤ cutoffCircS) (hcutoffConstant_bound : cubeLpNorm Q 2 (canonicalMaximizerPotentialDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0) * (cutoffDerivative + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ cutoffGradient) ≤ cutoffConstant) (hcenteredCutoffConstant_bound : 2 * (cubeScaleFactor Q * cutoffDerivative * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * (3 / 2 * (↑(Fintype.card (Fin d)) * poincareConst) * 3 ^ (↑d + 1) * cutoffCircOne)) + cubeLpNorm Q ⊤ cutoffGradient * (cubeBesovScaleWeight (-s) Q * (3 / 2 * (↑(Fintype.card (Fin d)) * poincareConst) * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cutoffCircS))) ≤ centeredCutoffConstant) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; have gradWeak := Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun; have fluxWeak := Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun; have gradCoeff := 3 ^ (↑d + s) * cubeBesovScaleWeight (-s) Q * BφS; have fluxCoeff := 3 ^ (↑d + t) * cubeBesovScaleWeight (-t) Q * BφT; |centeredResponseJOnCube Q (F.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(responseJPartitionDefectOnFamilyAtDepth F Q j p q) * √(childResponseJAverageOnFamilyAtDepth F Q j p q)) + Cosc * scaleSep * Ch04.restrictionResponseJObservableCubeSet Q p q a + (1 / 2 * ‖q0‖ * (↑(Fintype.card (Fin d)) * gradCoeff * gradWeak) + 1 / 2 * ‖p0‖ * (↑(Fintype.card (Fin d)) * fluxCoeff * fluxWeak)) + cutoffProductBridgeRHS Q s cutoffGradient (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q 1 p q q0 a.toFun) (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun) ‖Ch04.canonicalScalarResponseFluxAverageCubeSet Q Q p q a.toFun - q0‖ cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant

Deterministic assembled Section 5.3 estimate with all four displayed split terms replaced by their current deterministic manuscript bounds. This is the pointwise estimate to feed into the expectation step.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_responseJDifference_le_additivityError_cutoffBound_weakNorms_product {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (Q : TriadicCube d) (j : ℕ) (s t : ℝ) (φ : Vec d → ℝ) (p q p0 q0 : Vec d) {C B Cosc scaleSep BφS BφT cutoffDerivative : ℝ} (hC : 0 ≤ C) (hCut : ∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ C) (hφ_int : MeasureTheory.IntegrableOn φ (cubeSet Q) MeasureTheory.volume) (hRem_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => (1 - φ x) * topHalfEnergyDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q x) (cubeSet Q) MeasureTheory.volume) (hProduct_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredProductDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredGradientLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hFluxLinear_int : MeasureTheory.IntegrableOn (fun (x : Vec d) => φ x * centeredFluxLinearDensityOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 q0 x) (cubeSet Q) MeasureTheory.volume) (hGradField : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (φ x • canonicalMaximizerGradientDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q p0 x) i) (cubeSet Q) MeasureTheory.volume) (hFluxField : ∀ (i : Fin d), MeasureTheory.IntegrableOn (fun (x : Vec d) => (φ x • canonicalMaximizerFluxDefectOnCube Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) p q q0 x) i) (cubeSet Q) MeasureTheory.volume) (hMean : cubeAverage Q φ = 1) (hφ_meas : MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn (cubeSet Q))) (hφ_bound : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet Q), ‖φ x‖ ≤ B) (hOscPoint : ∀ R ∈ descendantsAtDepth Q j, ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet R), |cubeAverage R φ - φ x| ≤ Cosc * scaleSep) (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) (hφ_sub : tsupport φ ⊆ openCubeSet Q) (hcutoffDerivative : 0 ≤ cutoffDerivative) (hs_pos : 0 < s) (hs_lt_one : s < 1) (ht_pos : 0 < t) (hst : s + t ≤ 1) (hBφS : 0 ≤ BφS) (hBφT : 0 ≤ BφT) (hφDualS : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N φ ≤ BφS) (hφDualT : ∀ (N : ℕ), cubeBesovDualTestNorm Q t 2 1 N φ ≤ BφT) (hφMem : CubeBesovDualLocalMemLpGlobal Q 2 φ) (hcutoffGradient : MeasureTheory.MemLp (scalarCutoffGradientField φ) ⊤ (normalizedCubeMeasure Q)) (hcutoffSmooth : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => scalarCutoffGradientField φ x i) (hcutoffDeriv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => scalarCutoffGradientField φ x i) z‖ ≤ cutoffDerivative) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; have gradWeak := Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun; have fluxWeak := Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun; have gradCoeff := 3 ^ (↑d + s) * cubeBesovScaleWeight (-s) Q * BφS; have fluxCoeff := 3 ^ (↑d + t) * cubeBesovScaleWeight (-t) Q * BφT; have scaledGrad := cubeBesovScaleWeight (-s) Q * gradWeak; have scaledFlux := cubeBesovScaleWeight (-t) Q * fluxWeak; have productCoeff := cutoffProductScaledWeakNormCoeff Q s t cutoffDerivative (scalarCutoffGradientField φ); |centeredResponseJOnCube Q (F.coeffOn Q) p q p0 q0 - cutoffWeightedChildResponseJOnFamilyAtDepth F Q j φ p q| ≤ 2 * C * (√(responseJPartitionDefectOnFamilyAtDepth F Q j p q) * √(childResponseJAverageOnFamilyAtDepth F Q j p q)) + Cosc * scaleSep * Ch04.restrictionResponseJObservableCubeSet Q p q a + (1 / 2 * ‖q0‖ * (↑(Fintype.card (Fin d)) * gradCoeff * gradWeak) + 1 / 2 * ‖p0‖ * (↑(Fintype.card (Fin d)) * fluxCoeff * fluxWeak)) + productCoeff * (scaledGrad * scaledFlux)

Deterministic pointwise estimate with the product term in the final scaled-gradient/scaled-flux weak-norm form.