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

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

noncomputable def HCPolySupport.SmoothOverlapPartition.averagingField {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : Vec d → Vec d

The vector field obtained by averaging h on overlap cubes and blending the averages with a smooth overlap partition.

Equations

• P.averagingField h x i = ∑ S ∈ HCPolySupport.overlapCentersAtDepth Q j, P.weight S x * HCPolySupport.overlapCubeAverageVec S h i

@[simp]

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

theorem HCPolySupport.SmoothOverlapPartition.contDiff_averagingField_coord {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (i : Fin d) : ContDiff ℝ 1 fun (x : Vec d) => P.averagingField h x i

Each coordinate of the overlap averaging field is globally C¹, since it is a finite linear combination of the smooth partition weights.

noncomputable def HCPolySupport.SmoothOverlapPartition.averagingCompetitor {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : CubeVectorH1Function Q

The overlap averaging field packaged as a coordinatewise H¹ competitor on the parent cube.

Equations

• P.averagingCompetitor h = { coord := fun (i : Fin d) => HCPolySupport.H1Function.ofContDiffOnIsOpenBoundedConvexDomain ⋯ ⋯ }

@[simp]

theorem HCPolySupport.SmoothOverlapPartition.averagingCompetitor_toField_apply {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (x : Vec d) (i : Fin d) : (P.averagingCompetitor h).toField x i = P.averagingField h x i

@[simp]

theorem HCPolySupport.SmoothOverlapPartition.averagingCompetitor_coord_grad_apply {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (x : Vec d) (i k : Fin d) : ((P.averagingCompetitor h).coord i).grad x k = euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x

theorem HCPolySupport.SmoothOverlapPartition.euclideanCoordDeriv_averagingField_coord_eq_sum {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) (x : Vec d) (i k : Fin d) : euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x = ∑ S ∈ overlapCentersAtDepth Q j, euclideanCoordDeriv k (P.weight S) x * overlapCubeAverageVec S h i

Coordinate derivative of one component of the overlap averaging field.

theorem HCPolySupport.SmoothOverlapPartition.euclideanCoordDeriv_averagingField_coord_eq_sum_fluctuation {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 = ∑ S ∈ overlapCentersAtDepth Q j, euclideanCoordDeriv k (P.weight S) x * (overlapCubeAverageVec S h i - h x i)

Coordinate derivative of the overlap averaging field after subtracting the point value using the partition-of-unity cancellation.

theorem HCPolySupport.SmoothOverlapPartition.exists_euclideanCoordDeriv_averagingField_coord_sq_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {x : Vec d}, x ∈ openCubeSet Q → ∀ (i k : Fin d), euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x ^ 2 ≤ 3 ^ d * (C / (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, in the same localized fluctuation budget used by the residual estimate.

theorem HCPolySupport.SmoothOverlapPartition.exists_ofReal_euclideanCoordDeriv_averagingField_coord_sq_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {x : Vec d}, 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 * (C / (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

ENNReal pointwise scalar derivative estimate for the overlap averaging field. This is the form that can be integrated directly.

theorem HCPolySupport.SmoothOverlapPartition.exists_lintegral_ofReal_euclideanCoordDeriv_averagingField_coord_sq_le {d : ℕ} {Q : TriadicCube d} {j : ℕ} (P : SmoothOverlapPartition Q j) (h : Vec d → Vec d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (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 * (C / (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

Integrated scalar derivative estimate up to the localized overlap fluctuation indicator budget.

theorem HCPolySupport.SmoothOverlapPartition.exists_lintegral_ofReal_euclideanCoordDeriv_averagingField_coord_sq_le_vector_average {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 ∧ ∀ (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 * (C / (cubeScaleFactor Q / 3 ^ j)) ^ 2) * (3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S))

Integrated scalar derivative estimate after converting the localized indicator budget to the vector overlap fluctuation average.

theorem HCPolySupport.SmoothOverlapPartition.exists_cubeLpNorm_euclideanCoordDeriv_averagingField_coord_sq_le_vector_average_toReal {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 ∧ ∀ (i k : Fin d), (cubeLpNorm Q 2 fun (x : Vec d) => euclideanCoordDeriv k (fun (y : Vec d) => P.averagingField h y i) x) ^ 2 ≤ (ENNReal.ofReal (3 ^ d * (C / (cubeScaleFactor Q / 3 ^ j)) ^ 2) * (3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S))).toReal

Normalized scalar L² version of the integrated derivative estimate, still with the vector-overlap average as an ENNReal.toReal budget.

theorem HCPolySupport.SmoothOverlapPartition.exists_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)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (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 * (C / (cubeScaleFactor Q / 3 ^ j)) ^ 2 * (3 ^ d * ↑(Fintype.card (Fin d)) * cubeBesovOverlappingPositiveVectorDepthAverage Q h j)

Real-valued squared normalized scalar derivative bound in terms of the overlapping positive depth average.

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

Square-rooted normalized scalar derivative bound for the overlap averaging field. The scale appears as the inverse overlap side length (cubeScaleFactor Q / 3^j)^{-1}.