Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.AveragingGradientExplicit

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

noncomputable def HCPolySupport.SmoothOverlapPartition.scalarGradientConstant {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) : ℝ

Scalar derivative constant for the explicit overlap averaging gradient estimate.

Equations

• P.scalarGradientConstant = √(3 ^ d * (3 ^ d * ↑(Fintype.card (Fin d)))) * P.coordDerivConstant

theorem HCPolySupport.SmoothOverlapPartition.scalarGradientConstant_nonneg {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) : 0 ≤ P.scalarGradientConstant

noncomputable def HCPolySupport.SmoothOverlapPartition.gradientConstant {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) : ℝ

The constant bounding the sum of coordinate-gradient L² norms of the overlap averaging competitor, including both coordinate sums.

Equations

• P.gradientConstant = ↑(Fintype.card (Fin d)) * ↑(Fintype.card (Fin d)) * P.scalarGradientConstant

theorem HCPolySupport.SmoothOverlapPartition.gradientConstant_nonneg {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) : 0 ≤ P.gradientConstant

theorem HCPolySupport.SmoothOverlapPartition.euclideanCoordDeriv_averagingField_coord_sq_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i k : Fin d) : euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x ^ 2 ≤ 3 ^ d * (P.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)) ^ 2 * ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator (fun (y : Vec d) => (h y i - overlapCubeAverageVec S h i) ^ 2) x

Pointwise scalar derivative bound for the overlap averaging field with the explicit derivative constant stored in the partition.

theorem HCPolySupport.SmoothOverlapPartition.ofReal_euclideanCoordDeriv_averagingField_coord_sq_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) {x : Vec d} (hx : x ∈ openCubeSet Q) (i k : Fin d) : ENNReal.ofReal (euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x ^ 2) ≤ ENNReal.ofReal (3 ^ d * (P.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)) ^ 2) * ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator (fun (y : Vec d) => ENNReal.ofReal ((h y i - overlapCubeAverageVec S h i) ^ 2)) x

theorem HCPolySupport.SmoothOverlapPartition.lintegral_ofReal_euclideanCoordDeriv_averagingField_coord_sq_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (i k : Fin d) : ∫⁻ (x : Vec d), ENNReal.ofReal (euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x ^ 2) ∂normalizedCubeMeasure Q ≤ ENNReal.ofReal (3 ^ d * (P.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)) ^ 2) * ∫⁻ (x : Vec d), ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator (fun (y : Vec d) => ENNReal.ofReal ((h y i - overlapCubeAverageVec S h i) ^ 2)) x ∂normalizedCubeMeasure Q

theorem HCPolySupport.SmoothOverlapPartition.cubeLpNorm_euclideanCoordDeriv_averagingField_coord_sq_le_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)) (i k : Fin d) : (cubeLpNorm Q 2 fun (x : Vec d) => euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x) ^ 2 ≤ 3 ^ d * (P.coordDerivConstant / (cubeScaleFactor Q / 3 ^ j)) ^ 2 * (3 ^ d * ↑(Fintype.card (Fin d)) * cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

theorem HCPolySupport.SmoothOverlapPartition.cubeLpNorm_euclideanCoordDeriv_averagingField_coord_le_invScale_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)) (i k : Fin d) : (cubeLpNorm Q 2 fun (x : Vec d) => euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x) ≤ P.scalarGradientConstant / (cubeScaleFactor Q / 3 ^ j) * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

theorem HCPolySupport.SmoothOverlapPartition.gradientCoordL2NormSum_averagingCompetitor_le_volume_invScale_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)) : (P.averagingCompetitor h).gradientCoordL2NormSum ≤ cubeVolume Q ^ (1 / 2) * (P.gradientConstant / (cubeScaleFactor Q / 3 ^ j)) * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

theorem HCPolySupport.SmoothOverlapPartition.rpow_neg_mul_relativeGradientCoordL2NormSum_averagingCompetitor_le_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)) : Real.rpow 3 (-↑j) * (P.averagingCompetitor h).relativeGradientCoordL2NormSum ≤ P.gradientConstant * √(cubeBesovOverlappingPositiveVectorDepthAverage Q h j)