Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.AveragingResidual

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

theorem HCPolySupport.SmoothOverlapPartition.averagingField_const_of_mem_openCubeSet {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (c : Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) : P.averagingField (fun (x : Vec d) => c) x = c

The partition-parametrized averaging field preserves constants on the parent cube.

theorem HCPolySupport.SmoothOverlapPartition.sub_averagingField_apply_eq_sum_weighted_overlap_fluctuation {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i : Fin d) : (h x - P.averagingField h x) i = ∑ S ∈ overlapCentersAtDepth Q j, P.weight S x * (h x i - overlapCubeAverageVec S h i)

Coordinate form of the residual identity h - A_j h = sum_S phi_S (h - h_S).

theorem HCPolySupport.SmoothOverlapPartition.weight_le_one_of_mem_openCubeSet {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) {S : TriadicCube d} {x : Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hx : x ∈ openCubeSet Q) : P.weight S x ≤ 1

A partition weight belonging to an active overlap center is at most one on the parent cube.

theorem HCPolySupport.SmoothOverlapPartition.sub_averagingField_apply_sq_le_activeCard_mul_sum_overlap_fluctuation_sq {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i : Fin d) : (h x - P.averagingField h x) i ^ 2 ≤ ↑{S ∈ overlapCentersAtDepth Q j | P.weight S x ≠ 0}.card * ∑ S ∈ overlapCentersAtDepth Q j, (h x i - overlapCubeAverageVec S h i) ^ 2

Pointwise coordinate residual bound obtained from the partition identity and bounded active overlap. This is the local algebraic heart of the L² residual estimate; the subsequent integral step uses support containment and the finite-overlap comparison.

theorem HCPolySupport.SmoothOverlapPartition.sub_averagingField_apply_sq_le_activeCard_mul_activeSum_overlap_fluctuation_sq {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i : Fin d) : (h x - P.averagingField h x) i ^ 2 ≤ ↑{S ∈ overlapCentersAtDepth Q j | P.weight S x ≠ 0}.card * ∑ S ∈ overlapCentersAtDepth Q j with P.weight S x ≠ 0, (h x i - overlapCubeAverageVec S h i) ^ 2

Sharper pointwise coordinate residual bound retaining the active-center sum. This is the form used for the support-localized integral estimate.

theorem HCPolySupport.SmoothOverlapPartition.activeSum_overlap_fluctuation_sq_le_sum_openOverlap_indicator {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i : Fin d) : ∑ S ∈ overlapCentersAtDepth Q j with P.weight S x ≠ 0, (h x i - overlapCubeAverageVec S h i) ^ 2 ≤ ∑ S ∈ overlapCentersAtDepth Q j, (openOverlapCubeSet S).indicator (fun (y : Vec d) => (h y i - overlapCubeAverageVec S h i) ^ 2) x

Active terms in the residual estimate are supported in their corresponding open overlap cubes, so the active fluctuation sum is dominated by the indicator sum over all retained overlap centers.

theorem HCPolySupport.SmoothOverlapPartition.vecNormSq_sub_averagingField_le_activeCard_mul_activeSum_vecNormSq {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) ≤ ↑{S ∈ overlapCentersAtDepth Q j | P.weight S x ≠ 0}.card * ∑ S ∈ overlapCentersAtDepth Q j with P.weight S x ≠ 0, vecNormSq (h x - overlapCubeAverageVec S h)

Vector-valued pointwise residual bound, obtained by summing the coordinate active-center estimates.

theorem HCPolySupport.SmoothOverlapPartition.activeSum_vecNormSq_le_sum_openOverlap_indicator {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) : ∑ S ∈ overlapCentersAtDepth Q j with P.weight S x ≠ 0, vecNormSq (h x - overlapCubeAverageVec S h) ≤ ∑ S ∈ overlapCentersAtDepth Q j, (openOverlapCubeSet S).indicator (fun (y : Vec d) => vecNormSq (h y - overlapCubeAverageVec S h)) x

Vector-valued active sums are dominated by overlap-cube indicator sums, retaining the support information from the partition.

theorem HCPolySupport.SmoothOverlapPartition.exists_vecNormSq_sub_averagingField_le_activeBound_mul_sum_openOverlap_indicator {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : ∃ (M : ℕ), ∀ {x : Vec d}, x ∈ openCubeSet Q → vecNormSq (h x - P.averagingField h x) ≤ ↑M * ∑ S ∈ overlapCentersAtDepth Q j, (openOverlapCubeSet S).indicator (fun (y : Vec d) => vecNormSq (h y - overlapCubeAverageVec S h)) x

Pointwise residual energy estimate with the abstract active-cardinality constant from the partition.

theorem HCPolySupport.SmoothOverlapPartition.exists_ofReal_vecNormSq_sub_averagingField_le_activeBound_mul_sum_overlap_indicator {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : ∃ (M : ℕ), ∀ {x : Vec d}, x ∈ openCubeSet Q → ENNReal.ofReal (vecNormSq (h x - P.averagingField h x)) ≤ ↑M * ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator (fun (y : Vec d) => ENNReal.ofReal (vecNormSq (h y - overlapCubeAverageVec S h))) x

ENNReal pointwise residual energy estimate using closed overlap-cube indicators. This is the form designed to integrate against normalizedCubeMeasure Q.

theorem HCPolySupport.SmoothOverlapPartition.exists_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))) : ∃ (M : ℕ), ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - P.averagingField h x)) ∂normalizedCubeMeasure Q ≤ ↑M * 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S)

Integrated lintegral residual-energy estimate for the overlap averaging competitor. The only measurability input is the family of closed-overlap fluctuation indicators needed by the finite-sum integral comparison.

theorem HCPolySupport.SmoothOverlapPartition.exists_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))) : ∃ (M : ℕ), ↑M * 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 ≤ (↑M * 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 for the overlap averaging competitor, packaged from the lintegral estimate. The finiteness hypothesis is intentional: without it, ENNReal.toReal would turn an infinite upper bound into zero.

theorem HCPolySupport.SmoothOverlapPartition.exists_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)) : ∃ (C : ℝ), 0 ≤ C ∧ (cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ^ 2 ≤ C * cubeBesovOverlappingPositiveVectorDepthAverage Q h j

Squared residual estimate against the existing overlapping positive depth average. This is the residual half of the averaging-competitor estimate, before taking square roots.

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeLpNorm_sub_averagingField_le_mul_sqrt_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)) : ∃ (C : ℝ), 0 ≤ C ∧ (cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ≤ C * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeLpNorm_sq_sub_averagingField_le_mul_depthAverage_of_memLp_overlap {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)) : ∃ (C : ℝ), 0 ≤ C ∧ (cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ^ 2 ≤ C * cubeBesovOverlappingPositiveVectorDepthAverage Q h j

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeLpNorm_sub_averagingField_le_mul_sqrt_depthAverage_of_memLp_overlap {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)) : ∃ (C : ℝ), 0 ≤ C ∧ (cubeLpNorm Q 2 fun (x : Vec d) => h x - P.averagingField h x) ≤ C * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)