Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.CutoffBoundaryError

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

def HCPolySupport.cubeCoordInnerCollar {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) (i : Fin d) : Set (Vec d)

The coordinate collar where the i-direction derivative of an inner cube cutoff may be nonzero.

Equations

• HCPolySupport.cubeCoordInnerCollar Q ρ i = {x : HCPolySupport.Vec d | ρ * HCPolySupport.cubeRadius Q ≤ |x i - HCPolySupport.cubeCenter Q i|}

theorem HCPolySupport.measurableSet_cubeCoordInnerCollar {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) (i : Fin d) : MeasurableSet (cubeCoordInnerCollar Q ρ i)

theorem HCPolySupport.support_canonicalFun_fderiv_apply_basisVec_subset_cubeCoordInnerCollar {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (i : Fin d) : (Function.support fun (x : Vec d) => (fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x) (basisVec i)) ⊆ cubeCoordInnerCollar Q ρ₁ i

theorem HCPolySupport.support_canonicalFun_coordDeriv_mul_subset_cubeCoordInnerCollar {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (i : Fin d) (ψ : Vec d → ℝ) : (Function.support fun (x : Vec d) => (fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x) (basisVec i) * ψ x) ⊆ cubeCoordInnerCollar Q ρ₁ i

theorem HCPolySupport.norm_canonicalFun_coordDeriv_mul_le_of_collar_bound {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ B : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hB : 0 ≤ B) (i : Fin d) (ψ : Vec d → ℝ) (hψ : ∀ x ∈ cubeCoordInnerCollar Q ρ₁ i, ‖ψ x‖ ≤ B * ((ρ₂ - ρ₁) * cubeRadius Q)) (x : Vec d) : ‖(fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x) (basisVec i) * ψ x‖ ≤ B * quantitativeCubeCutoffGradientConst d

If a smooth test is at most B times the cutoff transition width on the coordinate collar, then the cutoff-derivative error is uniformly bounded.

theorem HCPolySupport.eLpNorm_canonicalFun_coordDeriv_mul_le_of_collar_bound {d : ℕ} {U : Set (Vec d)} (Q : TriadicCube d) {ρ₁ ρ₂ B : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hB : 0 ≤ B) (i : Fin d) (ψ : Vec d → ℝ) (hψ : ∀ x ∈ cubeCoordInnerCollar Q ρ₁ i, ‖ψ x‖ ≤ B * ((ρ₂ - ρ₁) * cubeRadius Q)) (hψm : MeasureTheory.AEStronglyMeasurable ψ (volumeMeasureOn U)) : MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x) (basisVec i) * ψ x) 2 (volumeMeasureOn U) ≤ ENNReal.ofReal (B * quantitativeCubeCutoffGradientConst d) * (volumeMeasureOn U) (cubeCoordInnerCollar Q ρ₁ i) ^ (1 / ENNReal.toReal 2)

L² version of norm_canonicalFun_coordDeriv_mul_le_of_collar_bound, localized to the coordinate collar where the derivative can be nonzero.