Coarse-graining support: #
Support.Deterministic.ConstantCoefficientDirichletBesov.AveragingResidualExplicit
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
noncomputable def
HCPolySupport.SmoothOverlapPartition.residualConstant
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
:
The explicit residual constant carried by a smooth overlap partition.
Equations
- P.residualConstant = √(↑P.activeCardBound * 3 ^ d * ↑(Fintype.card (Fin d)))
Instances For
theorem
HCPolySupport.SmoothOverlapPartition.residualConstant_nonneg
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
:
theorem
HCPolySupport.SmoothOverlapPartition.vecNormSq_sub_averagingField_le_activeBound_mul_sum_openOverlap_indicator
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
(h : Vec d → Vec d)
{x : Vec d}
(hx : x ∈ openCubeSet Q)
:
vecNormSq (h x - P.averagingField h x) ≤ ↑P.activeCardBound * ∑ S ∈ overlapCentersAtDepth Q j,
(openOverlapCubeSet S).indicator (fun (y : Vec d) => vecNormSq (h y - overlapCubeAverageVec S h)) x
Pointwise residual estimate with the explicit active-cardinality field of the partition.
theorem
HCPolySupport.SmoothOverlapPartition.ofReal_vecNormSq_sub_averagingField_le_activeBound_mul_sum_overlap_indicator
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
(h : Vec d → Vec d)
{x : Vec d}
(hx : x ∈ openCubeSet Q)
:
ENNReal.ofReal (vecNormSq (h x - P.averagingField h x)) ≤ ↑P.activeCardBound * ∑ S ∈ overlapCentersAtDepth Q j,
(overlapCubeSet S).indicator (fun (y : Vec d) => ENNReal.ofReal (vecNormSq (h y - overlapCubeAverageVec S h))) x
ENNReal pointwise residual estimate with the explicit active-cardinality
field.
theorem
HCPolySupport.SmoothOverlapPartition.lintegral_ofReal_vecNormSq_sub_averagingField_le
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
(h : Vec d → Vec d)
(hfQ :
∀ S ∈ overlapCentersAtDepth Q j,
AEMeasurable
((overlapCubeSet S).indicator fun (y : Vec d) => ENNReal.ofReal (vecNormSq (h y - overlapCubeAverageVec S h)))
(MeasureTheory.volume.restrict (cubeSet Q)))
:
∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - P.averagingField h x)) ∂normalizedCubeMeasure Q ≤ ↑P.activeCardBound * 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j,
∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S)
Integrated residual-energy estimate with the explicit active-cardinality field.
theorem
HCPolySupport.SmoothOverlapPartition.cubeLpNorm_sq_sub_averagingField_le
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
(h : Vec d → Vec d)
(hfQ :
∀ S ∈ overlapCentersAtDepth Q j,
AEMeasurable
((overlapCubeSet S).indicator fun (y : Vec d) => ENNReal.ofReal (vecNormSq (h y - overlapCubeAverageVec S h)))
(MeasureTheory.volume.restrict (cubeSet Q)))
(hfinite :
↑P.activeCardBound * 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j,
∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S) ≠ ⊤)
:
(cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ^ 2 ≤ (↑P.activeCardBound * 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j,
∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S)).toReal
Real squared L² residual estimate with the explicit active-cardinality
field.
theorem
HCPolySupport.SmoothOverlapPartition.cubeLpNorm_sq_sub_averagingField_le_mul_depthAverage
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
(h : Vec d → Vec d)
(hfQ :
∀ S ∈ overlapCentersAtDepth Q j,
AEMeasurable
((overlapCubeSet S).indicator fun (y : Vec d) => ENNReal.ofReal (vecNormSq (h y - overlapCubeAverageVec S h)))
(MeasureTheory.volume.restrict (cubeSet Q)))
(hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S))
:
(cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ^ 2 ≤ ↑P.activeCardBound * 3 ^ d * ↑(Fintype.card (Fin d)) * cubeBesovOverlappingPositiveVectorDepthAverage Q h j
Squared residual estimate against the overlapping positive depth average, with the explicit active-cardinality field.
theorem
HCPolySupport.SmoothOverlapPartition.cubeLpNorm_sub_averagingField_le_residualConstant_mul_sqrt_depthAverage
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
(P : SmoothOverlapPartition Q j)
(h : Vec d → Vec d)
(hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S))
:
(cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ≤ P.residualConstant * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)