Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.FaceVanishCollar

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

noncomputable def HCPolySupport.cubeLowerFaceProjection {d : ℕ} (Q : TriadicCube d) (i : Fin d) (x : Vec d) : Vec d

Projection onto the lower i-normal face, changing only coordinate i.

Equations

• HCPolySupport.cubeLowerFaceProjection Q i x = Function.update x i (HCPolySupport.cubeLowerFaceCoord Q i)

noncomputable def HCPolySupport.cubeUpperFaceProjection {d : ℕ} (Q : TriadicCube d) (i : Fin d) (x : Vec d) : Vec d

Projection onto the upper i-normal face, changing only coordinate i.

Equations

• HCPolySupport.cubeUpperFaceProjection Q i x = Function.update x i (HCPolySupport.cubeUpperFaceCoord Q i)

theorem HCPolySupport.cubeLowerFaceCoord_eq_cubeCenter_sub_cubeRadius {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeLowerFaceCoord Q i = cubeCenter Q i - cubeRadius Q

theorem HCPolySupport.cubeUpperFaceCoord_eq_cubeCenter_add_cubeRadius {d : ℕ} (Q : TriadicCube d) (i : Fin d) : cubeUpperFaceCoord Q i = cubeCenter Q i + cubeRadius Q

theorem HCPolySupport.norm_sub_cubeLowerFaceProjection_le {d : ℕ} (Q : TriadicCube d) (i : Fin d) (x : Vec d) : ‖x - cubeLowerFaceProjection Q i x‖ ≤ |x i - cubeLowerFaceCoord Q i|

theorem HCPolySupport.norm_sub_cubeUpperFaceProjection_le {d : ℕ} (Q : TriadicCube d) (i : Fin d) (x : Vec d) : ‖x - cubeUpperFaceProjection Q i x‖ ≤ |x i - cubeUpperFaceCoord Q i|

theorem HCPolySupport.norm_sub_le_mul_norm_sub_of_fderiv_bound {d : ℕ} {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {L : ℝ} (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (x y : Vec d) : ‖ψ x - ψ y‖ ≤ L * ‖x - y‖

theorem HCPolySupport.norm_le_mul_abs_sub_lowerFace_of_face_zero {d : ℕ} (Q : TriadicCube d) (i : Fin d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {L : ℝ} (hL : 0 ≤ L) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (x : Vec d) (hzero : ψ (cubeLowerFaceProjection Q i x) = 0) : ‖ψ x‖ ≤ L * |x i - cubeLowerFaceCoord Q i|

theorem HCPolySupport.norm_le_mul_abs_sub_upperFace_of_face_zero {d : ℕ} (Q : TriadicCube d) (i : Fin d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {L : ℝ} (hL : 0 ≤ L) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (x : Vec d) (hzero : ψ (cubeUpperFaceProjection Q i x) = 0) : ‖ψ x‖ ≤ L * |x i - cubeUpperFaceCoord Q i|

theorem HCPolySupport.face_distance_le_of_mem_scaledClosedCubeSet_coordInnerCollar {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₂_le_one : ρ₂ ≤ 1) (i : Fin d) {x : Vec d} (hxouter : x ∈ scaledClosedCubeSet Q ρ₂) (hxcollar : x ∈ cubeCoordInnerCollar Q ρ₁ i) : |x i - cubeLowerFaceCoord Q i| ≤ (1 - ρ₁) * cubeRadius Q ∨ |x i - cubeUpperFaceCoord Q i| ≤ (1 - ρ₁) * cubeRadius Q

In the inner coordinate collar, a point that still lies in the full cube is within (1 - ρ₁) * radius of one of the two i-normal faces.

theorem HCPolySupport.norm_le_of_face_zero_on_coordInnerCollar {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ L : ℝ} (hρ₂_le_one : ρ₂ ≤ 1) (i : Fin d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hL : 0 ≤ L) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) {x : Vec d} (hxouter : x ∈ scaledClosedCubeSet Q ρ₂) (hxcollar : x ∈ cubeCoordInnerCollar Q ρ₁ i) : ‖ψ x‖ ≤ L * ((1 - ρ₁) * cubeRadius Q)

Smooth functions vanishing on the two i-normal face projections are small on the coordinate collar, with the expected distance-to-face factor.

theorem HCPolySupport.cubeCoordInnerCollar_inter_openCubeSet_subset_cubeBoundaryLayer {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ_lt_one : ρ < 1) (i : Fin d) : cubeCoordInnerCollar Q ρ i ∩ openCubeSet Q ⊆ cubeBoundaryLayer Q (1 - ρ)

Inside the open cube, a coordinate inner collar is contained in an ordinary cube boundary layer. The boundary layer thickness is intentionally twice the sharp thickness; this avoids half-open face bookkeeping and is still asymptotically sharp enough for the cutoff limit.

theorem HCPolySupport.volumeMeasureOn_openCubeSet_cubeCoordInnerCollar_le_cubeBoundaryLayer {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ_lt_one : ρ < 1) (i : Fin d) : (volumeMeasureOn (openCubeSet Q)) (cubeCoordInnerCollar Q ρ i) ≤ MeasureTheory.volume (cubeBoundaryLayer Q (1 - ρ))

theorem HCPolySupport.norm_canonicalFun_coordDeriv_mul_le_of_face_zero {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ L A : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hρ₂_le_one : ρ₂ ≤ 1) (hL : 0 ≤ L) (hA_nonneg : 0 ≤ A) (hA_width : 1 - ρ₁ ≤ A * (ρ₂ - ρ₁)) (i : Fin d) (ψ : Vec d → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) (x : Vec d) : ‖(fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x) (basisVec i) * ψ x‖ ≤ L * A * quantitativeCubeCutoffGradientConst d

Face-vanishing version of the cutoff derivative error. The derivative of the cutoff supplies both localizations: it is supported in the coordinate collar and in the outer cutoff cube.

theorem HCPolySupport.eLpNorm_canonicalFun_coordDeriv_mul_le_of_face_zero {d : ℕ} {U : Set (Vec d)} (Q : TriadicCube d) {ρ₁ ρ₂ L A : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hρ₂_le_one : ρ₂ ≤ 1) (hL : 0 ≤ L) (hA_nonneg : 0 ≤ A) (hA_width : 1 - ρ₁ ≤ A * (ρ₂ - ρ₁)) (i : Fin d) (ψ : Vec d → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) x) (basisVec i) * ψ x) 2 (volumeMeasureOn U) ≤ ENNReal.ofReal (L * A * quantitativeCubeCutoffGradientConst d) * (volumeMeasureOn U) (cubeCoordInnerCollar Q ρ₁ i) ^ (1 / ENNReal.toReal 2)

L² form of the face-vanishing cutoff derivative error.

theorem HCPolySupport.tendsto_eLpNorm_canonicalFun_coordDeriv_mul_of_face_zero_of_collar_measure {d : ℕ} {U : Set (Vec d)} (Q : TriadicCube d) {ρ₁ ρ₂ : ℕ → ℝ} {L A : ℝ} (hρ₁ : ∀ (n : ℕ), 0 < ρ₁ n) (hρ₁₂ : ∀ (n : ℕ), ρ₁ n < ρ₂ n) (hρ₂_le_one : ∀ (n : ℕ), ρ₂ n ≤ 1) (hL : 0 ≤ L) (hA_nonneg : 0 ≤ A) (hA_width : ∀ (n : ℕ), 1 - ρ₁ n ≤ A * (ρ₂ n - ρ₁ n)) (i : Fin d) (ψ : Vec d → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) (hcollar : Filter.Tendsto (fun (n : ℕ) => (volumeMeasureOn U) (cubeCoordInnerCollar Q (ρ₁ n) i)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q (ρ₁ n) (ρ₂ n)) x) (basisVec i) * ψ x) 2 (volumeMeasureOn U)) Filter.atTop (nhds 0)

If the active coordinate collar has vanishing measure and the cutoff annuli have uniformly bounded aspect ratio, then the cutoff-gradient face error goes to zero in L².

noncomputable def HCPolySupport.faceCutoffInnerRadius (n : ℕ) : ℝ

A concrete inner radius schedule approaching the cube boundary. The denominator starts at 5 only to keep the associated boundary-layer thickness at most 1/2 for every index.

Equations

• HCPolySupport.faceCutoffInnerRadius n = 1 - 2 / (↑n + 5)

noncomputable def HCPolySupport.faceCutoffOuterRadius (n : ℕ) : ℝ

The matching outer radius schedule.

Equations

• HCPolySupport.faceCutoffOuterRadius n = 1 - 1 / (↑n + 5)

theorem HCPolySupport.faceCutoffInnerRadius_pos (n : ℕ) : 0 < faceCutoffInnerRadius n

theorem HCPolySupport.faceCutoffInnerRadius_lt_outer (n : ℕ) : faceCutoffInnerRadius n < faceCutoffOuterRadius n

theorem HCPolySupport.faceCutoffOuterRadius_le_one (n : ℕ) : faceCutoffOuterRadius n ≤ 1

theorem HCPolySupport.faceCutoffOuterRadius_nonneg (n : ℕ) : 0 ≤ faceCutoffOuterRadius n

theorem HCPolySupport.faceCutoffOuterRadius_lt_one (n : ℕ) : faceCutoffOuterRadius n < 1

theorem HCPolySupport.faceCutoffInnerOuter_width_control (n : ℕ) : 1 - faceCutoffInnerRadius n ≤ 2 * (faceCutoffOuterRadius n - faceCutoffInnerRadius n)

theorem HCPolySupport.faceCutoffInnerRadius_lt_one (n : ℕ) : faceCutoffInnerRadius n < 1

theorem HCPolySupport.tendsto_faceCutoffInnerRadius_one : Filter.Tendsto faceCutoffInnerRadius Filter.atTop (nhds 1)

noncomputable def HCPolySupport.faceCutoff {d : ℕ} (Q : TriadicCube d) (n : ℕ) : QuantitativeCubeCutoff Q (faceCutoffInnerRadius n) (faceCutoffOuterRadius n)

The canonical face-cutoff sequence used to trim smooth functions away from the cube boundary while letting the inner cube fill the whole cube.

Equations

• HCPolySupport.faceCutoff Q n = HCPolySupport.QuantitativeCubeCutoff.canonical Q (HCPolySupport.faceCutoffInnerRadius n) (HCPolySupport.faceCutoffOuterRadius n) ⋯ ⋯

theorem HCPolySupport.openCubeSet_subset_scaledClosedCubeSet_one {d : ℕ} (Q : TriadicCube d) : openCubeSet Q ⊆ scaledClosedCubeSet Q 1

The open triadic cube is contained in the closed concentric cube with relative radius 1.

noncomputable def HCPolySupport.faceCompactifyingCutoff {d : ℕ} (Q : TriadicCube d) : QuantitativeCubeCutoff Q 1 2

A fixed compactly supported cutoff that is identically 1 on the open triadic cube.

Equations

• HCPolySupport.faceCompactifyingCutoff Q = HCPolySupport.QuantitativeCubeCutoff.canonical Q 1 2 HCPolySupport.faceCompactifyingCutoff._proof_1 HCPolySupport.faceCompactifyingCutoff._proof_2

theorem HCPolySupport.faceCompactifyingCutoff_eq_one_on_openCubeSet {d : ℕ} (Q : TriadicCube d) {x : Vec d} (hx : x ∈ openCubeSet Q) : (faceCompactifyingCutoff Q).toFun x = 1

theorem HCPolySupport.tendsto_volumeMeasureOn_openCubeSet_cubeCoordInnerCollar_faceCutoffInnerRadius {d : ℕ} (Q : TriadicCube d) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => (volumeMeasureOn (openCubeSet Q)) (cubeCoordInnerCollar Q (faceCutoffInnerRadius n) i)) Filter.atTop (nhds 0)

theorem HCPolySupport.tendsto_eLpNorm_canonicalFun_coordDeriv_mul_of_face_zero_faceCutoffRadii {d : ℕ} (Q : TriadicCube d) (i : Fin d) (ψ : Vec d → ℝ) {L : ℝ} (hL : 0 ≤ L) (hψ : ContDiff ℝ (↑⊤) ψ) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (QuantitativeCubeCutoff.canonicalFun Q (faceCutoffInnerRadius n) (faceCutoffOuterRadius n)) x) (basisVec i) * ψ x) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)

The canonical face cutoff has vanishing derivative error along each coordinate for smooth functions that vanish on the two corresponding faces.

theorem HCPolySupport.tendsto_eLpNorm_euclideanCoordDeriv_faceCutoff_mul_of_face_zero {d : ℕ} (Q : TriadicCube d) (i : Fin d) (ψ : Vec d → ℝ) {L : ℝ} (hL : 0 ≤ L) (hψ : ContDiff ℝ (↑⊤) ψ) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanCoordDeriv i (faceCutoff Q n).toFun x * ψ x) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)

Boundary-error form of the face cutoff theorem, stated for the packaged QuantitativeCubeCutoff sequence.

theorem HCPolySupport.tendsto_eLpNorm_euclideanCoordDeriv_faceCutoff_mul_sub_of_face_zero {d : ℕ} (Q : TriadicCube d) (i : Fin d) (ψ : Vec d → ℝ) {L : ℝ} (hL : 0 ≤ L) (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) (hbound : ∀ (x : Vec d), ‖fderiv ℝ ψ x‖ ≤ L) (hlower_zero : ∀ (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => euclideanCoordDeriv i (fun (y : Vec d) => (faceCutoff Q n).toFun y * ψ y) x - euclideanCoordDeriv i ψ x) 2 (volumeMeasureOn (openCubeSet Q))) Filter.atTop (nhds 0)

Product-rule convergence for the face-cutoff sequence. For smooth compactly supported functions vanishing on the two i-faces, multiplying by the canonical inner cutoffs does not change the ith derivative in L²(openCubeSet Q).

noncomputable def HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSet {d : ℕ} (Q : TriadicCube d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) (hlower_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : H10Function (openCubeSet Q)

A smooth compactly supported function on a cube whose trace vanishes on every coordinate face belongs to the zero-trace H¹₀ closure. The approximants are the canonical inner face cutoffs times the function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSet_toFun {d : ℕ} (Q : TriadicCube d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) (hlower_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : (ofContDiffFaceZeroOnOpenCubeSet Q hψ hψ_compact hlower_zero hupper_zero).toFun = ψ

@[simp]

theorem HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSet_grad {d : ℕ} (Q : TriadicCube d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ_compact : HasCompactSupport ψ) (hlower_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : (ofContDiffFaceZeroOnOpenCubeSet Q hψ hψ_compact hlower_zero hupper_zero).grad = fun (x : Vec d) (i : Fin d) => (fderiv ℝ ψ x) (basisVec i)

noncomputable def HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSetNoCompact {d : ℕ} (Q : TriadicCube d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hlower_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : H10Function (openCubeSet Q)

A smooth function on a cube whose trace vanishes on every coordinate face belongs to the zero-trace H¹₀ closure. The proof first multiplies by a fixed smooth cutoff that is identically 1 on the cube, so no compact-support hypothesis is needed on the original function.

Equations

• HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSetNoCompact Q hψ hlower_zero hupper_zero = HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSet Q ⋯ ⋯ ⋯ ⋯

theorem HCPolySupport.H10Function.ofContDiffFaceZeroOnOpenCubeSetNoCompact_toFun_ae {d : ℕ} (Q : TriadicCube d) {ψ : Vec d → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hlower_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeLowerFaceProjection Q i x) = 0) (hupper_zero : ∀ (i : Fin d) (x : Vec d), ψ (cubeUpperFaceProjection Q i x) = 0) : (ofContDiffFaceZeroOnOpenCubeSetNoCompact Q hψ hlower_zero hupper_zero).toFun =ᵐ[volumeMeasureOn (openCubeSet Q)] ψ