Coarse-graining support: Support.Sobolev.Foundations.QuantitativeCutoff

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

Quantitative smooth cutoffs

This file provides the quantitative cutoff interfaces used by local Sobolev and Caccioppoli arguments. The ball version is the standard radial cutoff between two concentric balls. The cube version is the analogous cutoff between two concentric subcubes of a triadic cube.

The derivative bounds are expressed using dimensional constants. The default norm on Vec d is the product/sup norm, so Euclidean-ball cutoffs acquire dimension factors when their derivatives are measured with Lean's operator norm.

noncomputable def HCPolySupport.quantitativeBallCutoffGradientConst (d : ℕ) : ℝ

Dimensional first-derivative constant for the ball cutoff interface.

The factor d accounts for measuring derivatives on Vec d using the default sup/product norm.

Equations

• HCPolySupport.quantitativeBallCutoffGradientConst d = 8 * ↑d * HCPolySupport.smoothTransitionProfile.derivBound

noncomputable def HCPolySupport.quantitativeBallCutoffHessianConst (d : ℕ) : ℝ

Dimensional Hessian constant for the ball cutoff interface.

Equations

• HCPolySupport.quantitativeBallCutoffHessianConst d = 32 * ↑d ^ 2 * max 1 (max HCPolySupport.smoothTransitionProfile.derivBound HCPolySupport.smoothTransitionProfile.secondDerivBound)

noncomputable def HCPolySupport.quantitativeCubeCutoffGradientConst (d : ℕ) : ℝ

Dimensional first-derivative constant for the cube cutoff interface.

Equations

• HCPolySupport.quantitativeCubeCutoffGradientConst d = 8 * ↑d * HCPolySupport.smoothTransitionProfile.derivBound

noncomputable def HCPolySupport.quantitativeCubeCutoffHessianConst (d : ℕ) : ℝ

Dimensional Hessian constant for the cube cutoff interface.

Equations

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

structure HCPolySupport.QuantitativeBallCutoff {d : ℕ} (x₀ : Vec d) (r R : ℝ) : Type

A quantitative smooth cutoff between two concentric balls.

• toFun : Vec d → ℝ

  The smooth compactly supported scalar cutoff in [0, 1], equal to one on the inner ball and supported in the outer ball.

• smooth : ContDiff ℝ (↑⊤) self.toFun
• hasCompactSupport : HasCompactSupport self.toFun
• support_subset : tsupport self.toFun ⊆ euclideanBall x₀ R
• nonneg (x : Vec d) : 0 ≤ self.toFun x
• le_one (x : Vec d) : self.toFun x ≤ 1
• eq_one_on_inner (x : Vec d) : x ∈ euclideanBall x₀ r → self.toFun x = 1
• gradient_bound (x : Vec d) : ‖fderiv ℝ self.toFun x‖ ≤ quantitativeBallCutoffGradientConst d / (R - r)
• hessian_bound (x : Vec d) : ‖iteratedFDeriv ℝ 2 self.toFun x‖ ≤ quantitativeBallCutoffHessianConst d / (R - r) ^ 2

@[instance_reducible]

instance HCPolySupport.QuantitativeBallCutoff.instCoeFunForallVecReal {d : ℕ} {x₀ : Vec d} {r R : ℝ} : CoeFun (QuantitativeBallCutoff x₀ r R) fun (x : QuantitativeBallCutoff x₀ r R) => Vec d → ℝ

Equations

• HCPolySupport.QuantitativeBallCutoff.instCoeFunForallVecReal = { coe := fun (η : HCPolySupport.QuantitativeBallCutoff x₀ r R) => η.toFun }

noncomputable def HCPolySupport.QuantitativeBallCutoff.canonicalFun {d : ℕ} (x₀ : Vec d) (r s : ℝ) : Vec d → ℝ

Canonical smooth ball cutoff formula using Real.smoothTransition.

The extra support radius s leaves a collar between the support and B_R, which is necessary for tsupport to be contained in the open ball.

Equations

• HCPolySupport.QuantitativeBallCutoff.canonicalFun x₀ r s = HCPolySupport.smoothTransitionProfile.quantitativeProfile.ballCutoff x₀ r s

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_smooth {d : ℕ} (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) : ContDiff ℝ (↑⊤) (canonicalFun x₀ r s)

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_hasCompactSupport {d : ℕ} (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) : HasCompactSupport (canonicalFun x₀ r s)

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_tsupport_subset_euclideanBall {d : ℕ} (x₀ : Vec d) {r s R : ℝ} (hr : 0 < r) (hrs : r < s) (hsR : s < R) : tsupport (canonicalFun x₀ r s) ⊆ euclideanBall x₀ R

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_nonneg {d : ℕ} (x₀ : Vec d) (r s : ℝ) (x : Vec d) : 0 ≤ canonicalFun x₀ r s x

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_le_one {d : ℕ} (x₀ : Vec d) (r s : ℝ) (x : Vec d) : canonicalFun x₀ r s x ≤ 1

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_eq_one_on_inner {d : ℕ} {x₀ : Vec d} {r s : ℝ} (hr : 0 < r) (hrs : r < s) {x : Vec d} (hx : x ∈ euclideanBall x₀ r) : canonicalFun x₀ r s x = 1

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_gradient_bound {d : ℕ} (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) (x : Vec d) : ‖fderiv ℝ (canonicalFun x₀ r s) x‖ ≤ smoothTransitionProfile.derivBound * (2 * ↑d / (s - r))

theorem HCPolySupport.QuantitativeBallCutoff.canonicalFun_hessian_bound {d : ℕ} (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (canonicalFun x₀ r s) x‖ ≤ 2 * max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) * (2 * ↑d / (s - r)) ^ 2

theorem HCPolySupport.QuantitativeBallCutoff.exists_bound_fderiv_canonicalFun {d : ℕ} (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖fderiv ℝ (canonicalFun x₀ r s) x‖ ≤ C

theorem HCPolySupport.QuantitativeBallCutoff.exists_bound_hessian_canonicalFun {d : ℕ} (x₀ : Vec d) {r s : ℝ} (hr : 0 < r) (hrs : r < s) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖iteratedFDeriv ℝ 2 (canonicalFun x₀ r s) x‖ ≤ C

noncomputable def HCPolySupport.QuantitativeBallCutoff.canonical {d : ℕ} (x₀ : Vec d) (r R : ℝ) (hr : 0 < r) (hrR : r < R) : QuantitativeBallCutoff x₀ r R

Canonical quantitative ball cutoff between B_r(x₀) and B_R(x₀), using the midpoint radius (r + R) / 2 as transition scale.

Equations

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

structure HCPolySupport.QuantitativeCubeCutoff {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) : Type

A quantitative smooth cutoff between two concentric subcubes of a triadic cube.

• toFun : Vec d → ℝ

  The smooth compactly supported scalar cutoff in [0, 1], equal to one on the inner closed subcube and supported in the outer open subcube.

• smooth : ContDiff ℝ (↑⊤) self.toFun
• hasCompactSupport : HasCompactSupport self.toFun
• support_subset : Function.support self.toFun ⊆ scaledOpenCubeSet Q ρ₂
• nonneg (x : Vec d) : 0 ≤ self.toFun x
• le_one (x : Vec d) : self.toFun x ≤ 1
• eq_one_on_inner (x : Vec d) : x ∈ scaledClosedCubeSet Q ρ₁ → self.toFun x = 1
• gradient_bound (x : Vec d) : ‖fderiv ℝ self.toFun x‖ ≤ quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)
• hessian_bound (x : Vec d) : ‖iteratedFDeriv ℝ 2 self.toFun x‖ ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2

@[instance_reducible]

instance HCPolySupport.QuantitativeCubeCutoff.instCoeFunForallVecReal {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} : CoeFun (QuantitativeCubeCutoff Q ρ₁ ρ₂) fun (x : QuantitativeCubeCutoff Q ρ₁ ρ₂) => Vec d → ℝ

Equations

• HCPolySupport.QuantitativeCubeCutoff.instCoeFunForallVecReal = { coe := fun (η : HCPolySupport.QuantitativeCubeCutoff Q ρ₁ ρ₂) => η.toFun }

noncomputable def HCPolySupport.QuantitativeCubeCutoff.canonicalFun {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) : Vec d → ℝ

Canonical smooth cube cutoff formula using Real.smoothTransition.

Equations

• HCPolySupport.QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ = HCPolySupport.smoothTransitionProfile.quantitativeProfile.cubeCutoff Q ρ₁ ρ₂

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_smooth {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : ContDiff ℝ (↑⊤) (canonicalFun Q ρ₁ ρ₂)

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_nonneg {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (x : Vec d) : 0 ≤ canonicalFun Q ρ₁ ρ₂ x

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_le_one {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (x : Vec d) : canonicalFun Q ρ₁ ρ₂ x ≤ 1

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_eq_one_on_inner {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {x : Vec d} (hx : x ∈ scaledClosedCubeSet Q ρ₁) : canonicalFun Q ρ₁ ρ₂ x = 1

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_support_subset {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : Function.support (canonicalFun Q ρ₁ ρ₂) ⊆ scaledOpenCubeSet Q ρ₂

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_tsupport_subset_scaledClosedCubeSet {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : tsupport (canonicalFun Q ρ₁ ρ₂) ⊆ scaledClosedCubeSet Q ρ₂

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_fderiv_apply_basisVec_eq_zero_of_abs_sub_center_lt_inner {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {i : Fin d} {x : Vec d} (hx : |x i - cubeCenter Q i| < ρ₁ * cubeRadius Q) : (fderiv ℝ (canonicalFun Q ρ₁ ρ₂) x) (basisVec i) = 0

The canonical product cutoff has zero coordinate derivative away from the corresponding coordinate collar.

theorem HCPolySupport.QuantitativeCubeCutoff.support_fderiv_canonicalFun_apply_basisVec_subset_coord_abs_ge_inner {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (i : Fin d) : (Function.support fun (x : Vec d) => (fderiv ℝ (canonicalFun Q ρ₁ ρ₂) x) (basisVec i)) ⊆ {x : Vec d | ρ₁ * cubeRadius Q ≤ |x i - cubeCenter Q i|}

Support form of canonicalFun_fderiv_apply_basisVec_eq_zero_of_abs_sub_center_lt_inner.

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

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_gradient_bound {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (x : Vec d) : ‖fderiv ℝ (canonicalFun Q ρ₁ ρ₂) x‖ ≤ ↑d * smoothTransitionProfile.derivBound * (2 / ((ρ₂ - ρ₁) * cubeRadius Q))

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_hessian_bound {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (canonicalFun Q ρ₁ ρ₂) x‖ ≤ 2 * ↑d ^ 2 * (max 1 (max smoothTransitionProfile.derivBound smoothTransitionProfile.secondDerivBound) * (2 / ((ρ₂ - ρ₁) * cubeRadius Q))) ^ 2

theorem HCPolySupport.QuantitativeCubeCutoff.canonicalFun_hasCompactSupport {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : HasCompactSupport (canonicalFun Q ρ₁ ρ₂)

theorem HCPolySupport.QuantitativeCubeCutoff.exists_bound_fderiv_canonicalFun {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖fderiv ℝ (canonicalFun Q ρ₁ ρ₂) x‖ ≤ C

theorem HCPolySupport.QuantitativeCubeCutoff.exists_bound_hessian_canonicalFun {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖iteratedFDeriv ℝ 2 (canonicalFun Q ρ₁ ρ₂) x‖ ≤ C

noncomputable def HCPolySupport.QuantitativeCubeCutoff.canonical {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : QuantitativeCubeCutoff Q ρ₁ ρ₂

Canonical quantitative cube cutoff between the concentric subcubes scaledClosedCubeSet Q ρ₁ and scaledOpenCubeSet Q ρ₂.

Equations

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