Coarse-graining support: Support.Sobolev.Foundations.Cutoff.Cube

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

Cube cutoffs from one-dimensional profiles

This file contains the coordinate-product construction for smooth cutoffs between concentric subcubes of a triadic cube.

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

Closed concentric subcube of relative radius ρ inside a triadic cube.

Equations

• HCPolySupport.scaledClosedCubeSet Q ρ = {x : HCPolySupport.Vec d | ∀ (i : Fin d), |x i - HCPolySupport.cubeCenter Q i| ≤ ρ * HCPolySupport.cubeRadius Q}

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

Open concentric subcube of relative radius ρ inside a triadic cube.

Equations

• HCPolySupport.scaledOpenCubeSet Q ρ = {x : HCPolySupport.Vec d | ∀ (i : Fin d), |x i - HCPolySupport.cubeCenter Q i| < ρ * HCPolySupport.cubeRadius Q}

theorem HCPolySupport.scaledClosedCubeSet_subset_metricClosedBall {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ : 0 ≤ ρ) : scaledClosedCubeSet Q ρ ⊆ Metric.closedBall (cubeCenter Q) (ρ * cubeRadius Q)

theorem HCPolySupport.isClosed_scaledClosedCubeSet {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) : IsClosed (scaledClosedCubeSet Q ρ)

theorem HCPolySupport.isCompact_scaledClosedCubeSet {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ : 0 ≤ ρ) : IsCompact (scaledClosedCubeSet Q ρ)

noncomputable def HCPolySupport.QuantitativeTransitionProfile.cubeArgument {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (i : Fin d) (x : Vec d) : ℝ

Squared coordinate interpolation variable for the ith face of a cube cutoff.

Equations

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

noncomputable def HCPolySupport.QuantitativeTransitionProfile.cubeCutoff {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (x : Vec d) : ℝ

Coordinate-product cube cutoff generated by a one-dimensional profile.

Equations

• θ.cubeCutoff Q ρ₁ ρ₂ x = ∏ i : Fin d, θ.toFun (HCPolySupport.QuantitativeTransitionProfile.cubeArgument Q ρ₁ ρ₂ i x)

noncomputable def HCPolySupport.QuantitativeTransitionProfile.cubeFactor {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (i : Fin d) (x : Vec d) : ℝ

Single profile factor appearing in the coordinate-product cube cutoff.

Equations

• θ.cubeFactor Q ρ₁ ρ₂ i x = θ.toFun (HCPolySupport.QuantitativeTransitionProfile.cubeArgument Q ρ₁ ρ₂ i x)

noncomputable def HCPolySupport.QuantitativeTransitionProfile.partialCubeCutoff {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (u : Finset (Fin d)) (x : Vec d) : ℝ

Partial coordinate-product used to build the full cube cutoff by induction over a finite set of coordinates.

Equations

• θ.partialCubeCutoff Q ρ₁ ρ₂ u x = ∏ i ∈ u, θ.cubeFactor Q ρ₁ ρ₂ i x

theorem HCPolySupport.QuantitativeTransitionProfile.fderiv_cubeArgument_apply_basisVec {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (i j : Fin d) (x : Vec d) : (fderiv ℝ (cubeArgument Q ρ₁ ρ₂ i) x) (basisVec j) = -(2 * (x i - cubeCenter Q i) * if j = i then 1 else 0) / ((ρ₂ * cubeRadius Q) ^ 2 - (ρ₁ * cubeRadius Q) ^ 2)

Exact coordinate-direction derivative of the one-dimensional cube argument.

theorem HCPolySupport.QuantitativeTransitionProfile.differentiableAt_cubeArgument {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (i : Fin d) (x : Vec d) : DifferentiableAt ℝ (cubeArgument Q ρ₁ ρ₂ i) x

The cube cutoff argument is differentiable whenever the annulus radii are strictly ordered.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_fderiv_cubeArgument_le_of_mem_scaledClosedCubeSet {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {i : Fin d} {x : Vec d} (hx : x ∈ scaledClosedCubeSet Q ρ₂) : ‖fderiv ℝ (cubeArgument Q ρ₁ ρ₂ i) x‖ ≤ 2 / ((ρ₂ - ρ₁) * cubeRadius Q)

On the outer closed cube, each one-dimensional cube argument has the expected first-derivative scale.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_iteratedFDeriv_two_cubeArgument_le {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (i : Fin d) (x : Vec d) : ‖iteratedFDeriv ℝ 2 (cubeArgument Q ρ₁ ρ₂ i) x‖ ≤ 2 / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2

Global second-derivative bound for each one-dimensional cube argument.

theorem HCPolySupport.QuantitativeTransitionProfile.cubeFactor_contDiff_two {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (i : Fin d) : ContDiff ℝ (↑2) (θ.cubeFactor Q ρ₁ ρ₂ i)

theorem HCPolySupport.QuantitativeTransitionProfile.fderiv_cubeFactor_eq_zero_of_abs_sub_center_lt_inner {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {i : Fin d} {x : Vec d} (hx : |x i - cubeCenter Q i| < ρ₁ * cubeRadius Q) : fderiv ℝ (θ.cubeFactor Q ρ₁ ρ₂ i) x = 0

Inside the ith inner slab, the ith one-dimensional cube factor is locally constant, hence its full Frechet derivative vanishes.

theorem HCPolySupport.QuantitativeTransitionProfile.fderiv_cubeFactor_apply_basisVec_eq_zero_of_ne {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {i k : Fin d} (hik : i ≠ k) (x : Vec d) : (fderiv ℝ (θ.cubeFactor Q ρ₁ ρ₂ k) x) (basisVec i) = 0

A coordinate direction differentiates only the matching cube factor.

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

The canonical coordinate-product cutoff has zero i-direction derivative away from the i-normal transition collar.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_iteratedFDeriv_one_cubeFactor_le_of_mem_scaledClosedCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {i : Fin d} {x : Vec d} (hx : x ∈ scaledClosedCubeSet Q ρ₂) : ‖iteratedFDeriv ℝ 1 (θ.cubeFactor Q ρ₁ ρ₂ i) x‖ ≤ θ.derivBound * (2 / ((ρ₂ - ρ₁) * cubeRadius Q))

theorem HCPolySupport.QuantitativeTransitionProfile.norm_iteratedFDeriv_two_cubeFactor_le_of_mem_scaledClosedCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {i : Fin d} {x : Vec d} (hx : x ∈ scaledClosedCubeSet Q ρ₂) : ‖iteratedFDeriv ℝ 2 (θ.cubeFactor Q ρ₁ ρ₂ i) x‖ ≤ 2 * max 1 (max θ.derivBound θ.secondDerivBound) * (2 / ((ρ₂ - ρ₁) * cubeRadius Q)) ^ 2

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_smooth {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : ContDiff ℝ (↑⊤) (θ.cubeCutoff Q ρ₁ ρ₂)

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_nonneg {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (x : Vec d) : 0 ≤ θ.cubeCutoff Q ρ₁ ρ₂ x

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_le_one {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (x : Vec d) : θ.cubeCutoff Q ρ₁ ρ₂ x ≤ 1

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_eq_one_of_mem_scaledClosedCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {x : Vec d} (hx : x ∈ scaledClosedCubeSet Q ρ₁) : θ.cubeCutoff Q ρ₁ ρ₂ x = 1

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_eq_zero_of_notMem_scaledOpenCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) {x : Vec d} (hx : x ∉ scaledOpenCubeSet Q ρ₂) : θ.cubeCutoff Q ρ₁ ρ₂ x = 0

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_support_subset_scaledOpenCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : Function.support (θ.cubeCutoff Q ρ₁ ρ₂) ⊆ scaledOpenCubeSet Q ρ₂

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_support_subset_scaledClosedCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : Function.support (θ.cubeCutoff Q ρ₁ ρ₂) ⊆ scaledClosedCubeSet Q ρ₂

theorem HCPolySupport.QuantitativeTransitionProfile.cubeCutoff_tsupport_subset_scaledClosedCubeSet {d : ℕ} (θ : QuantitativeTransitionProfile) {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) : tsupport (θ.cubeCutoff Q ρ₁ ρ₂) ⊆ scaledClosedCubeSet Q ρ₂

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

Global second-derivative bound for the coordinate-product cube cutoff.

theorem HCPolySupport.QuantitativeTransitionProfile.norm_fderiv_cubeCutoff_le {d : ℕ} (θ : QuantitativeTransitionProfile) (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (x : Vec d) : ‖fderiv ℝ (θ.cubeCutoff Q ρ₁ ρ₂) x‖ ≤ ↑d * θ.derivBound * (2 / ((ρ₂ - ρ₁) * cubeRadius Q))

Global first-derivative bound for the coordinate-product cube cutoff.