Coarse-graining support: #
Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.CutoffOscillation
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
CutoffOscillation #
Cutoff oscillation bounds.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_cutoffOscillationTermOnCubeAtDepth_le_osc_mul_responseJOnCube
{d : ℕ}
(Q : TriadicCube d)
(a : Ch02.CoeffOn (Ch02.cubeDomain Q))
(j : ℕ)
(φ : Vec d → ℝ)
(p q : Vec d)
{osc : ℝ}
(hOsc_int :
∀ R ∈ descendantsAtDepth Q j,
MeasureTheory.IntegrableOn (fun (x : Vec d) => (cubeAverage R φ - φ x) * topHalfEnergyDensityOnCube Q a p q x)
(cubeSet R) MeasureTheory.volume)
(hOscPoint : ∀ R ∈ descendantsAtDepth Q j, ∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet R), |cubeAverage R φ - φ x| ≤ osc)
:
Second manuscript term: the cutoff oscillation is bounded by its childwise oscillation size times the parent response.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_cutoffOscillationTermOnCubeAtDepth_le_scale_mul_responseJOnCube_of_ae_bounded_cutoff
{d : ℕ}
(Q : TriadicCube d)
(a : Ch02.CoeffOn (Ch02.cubeDomain Q))
(j : ℕ)
{φ : Vec d → ℝ}
{B C scaleSep : ℝ}
(p q : Vec d)
(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| ≤ C * scaleSep)
:
|cutoffOscillationTermOnCubeAtDepth Q a j φ p q| ≤ C * scaleSep * Ch02.responseJ (Ch02.cubeDomain Q) a p q
Cutoff-oscillation bound with the product integrability discharged from a bounded cutoff.
theorem
HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_cutoffOscillationTerm_le_scale_mul_responseJObservableSet
{d : ℕ}
[NeZero d]
(a : RegCoeffField d)
(ha : Ch04.AELocallyUniformlyEllipticField a)
(Q : TriadicCube d)
(j : ℕ)
{φ : Vec d → ℝ}
{B C scaleSep : ℝ}
(p q : Vec d)
(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| ≤ C * scaleSep)
:
|cutoffOscillationTermOnCubeAtDepth Q ((Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha).coeffOn Q) j φ p
q| ≤ C * scaleSep * Ch04.restrictionResponseJObservableCubeSet Q p q a
Law-facing form of the cutoff-oscillation bound for the Ch4 dependent triadic coefficient family.