CutoffData

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The per-core cutoff datum

For the per-core energy bound (local_block_energy, T2) behind the fixed-phase variance (Proposition 4.3) we need, for each core coreBox ℓ σ k, a smooth cutoff η that is 1 on the core, supported in the ℓ-enlargement, with the two integral estimates of e.corridor.cutoff:

• support-volume bound (vol (supp η ∩ U)).toReal ≤ (3ℓ)^d;
• squared-gradient bound ∫_U Σᵢ (∂ᵢ η)² ≤ d · (16/ℓ)² · (3ℓ)^d.

The cutoff is the boxCutoff for the closed core box (which is exactly Set.Icc (coreLo ℓ σ k) (coreHi ℓ σ k)) with margin ℓ. The gradient integral is finite because the gradient is supported in the (closed, bounded) enlargement Set.Icc (coreLo − ℓ) (coreHi + ℓ): off that enlargement η vanishes on an open set, so its Fréchet derivative is zero there.

The core box as a closed axis box

def HCPolySupport.coreLo {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Vec d

The lower corner of the closed core box.

Equations

• HCPolySupport.coreLo ℓ σ k i = σ i + ↑(k i) * ℓ + 1

def HCPolySupport.coreHi {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Vec d

The upper corner of the closed core box.

Equations

• HCPolySupport.coreHi ℓ σ k i = σ i + (↑(k i) + 1) * ℓ - 1

theorem HCPolySupport.coreBox_eq_Icc {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : coreBox ℓ σ k = Set.Icc (coreLo ℓ σ k) (coreHi ℓ σ k)

theorem HCPolySupport.coreHi_sub_coreLo {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (i : Fin d) : coreHi ℓ σ k i - coreLo ℓ σ k i = ℓ - 2

Side length hi − lo = ℓ − 2 in every coordinate.

theorem HCPolySupport.coreLo_le_coreHi {d : ℕ} {ℓ : ℝ} (hℓ : 2 ≤ ℓ) (σ : Vec d) (k : Fin d → ℤ) : coreLo ℓ σ k ≤ coreHi ℓ σ k

The per-core cutoff

noncomputable def HCPolySupport.coreCutoff {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Vec d → ℝ

The per-core smooth cutoff: boxCutoff of the closed core box with margin ℓ.

Equations

• HCPolySupport.coreCutoff ℓ σ k = HCPolySupport.boxCutoff (HCPolySupport.coreLo ℓ σ k) (HCPolySupport.coreHi ℓ σ k) ℓ

theorem HCPolySupport.coreCutoff_contDiff {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : ContDiff ℝ (↑⊤) (coreCutoff ℓ σ k)

theorem HCPolySupport.coreCutoff_mem_Icc {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (x : Vec d) : coreCutoff ℓ σ k x ∈ Set.Icc 0 1

theorem HCPolySupport.coreCutoff_deriv_bound {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) (k : Fin d → ℤ) (x : Vec d) (i : Fin d) : |(fderiv ℝ (coreCutoff ℓ σ k) x) (basisVec i)| ≤ 16 / ℓ

theorem HCPolySupport.coreCutoff_eq_one_of_mem_coreBox {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) (k : Fin d → ℤ) {x : Vec d} (hx : x ∈ coreBox ℓ σ k) : coreCutoff ℓ σ k x = 1

On the core box the cutoff is identically 1.

The closed enlargement and the support of the gradient

def HCPolySupport.coreEnlarge {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Set (Vec d)

The closed ℓ-enlargement of the core box.

Equations

• HCPolySupport.coreEnlarge ℓ σ k = Set.Icc (fun (i : Fin d) => HCPolySupport.coreLo ℓ σ k i - ℓ) fun (i : Fin d) => HCPolySupport.coreHi ℓ σ k i + ℓ

theorem HCPolySupport.measurableSet_coreEnlarge {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : MeasurableSet (coreEnlarge ℓ σ k)

theorem HCPolySupport.coreCutoff_fderiv_eq_zero_of_notMem {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) (k : Fin d → ℤ) {x : Vec d} (hx : x ∉ coreEnlarge ℓ σ k) : fderiv ℝ (coreCutoff ℓ σ k) x = 0

Off the enlargement, η vanishes on an open set, so its Fréchet derivative is zero.

theorem HCPolySupport.coreCutoff_sqGrad_eq_zero_of_notMem {d : ℕ} {ℓ : ℝ} (hℓ : 0 < ℓ) (σ : Vec d) (k : Fin d → ℤ) {x : Vec d} (hx : x ∉ coreEnlarge ℓ σ k) : ∑ i : Fin d, (fderiv ℝ (coreCutoff ℓ σ k) x) (basisVec i) ^ 2 = 0

The squared gradient vanishes off the enlargement.

The two integral estimates

theorem HCPolySupport.volume_coreEnlarge_toReal {d : ℕ} {ℓ : ℝ} (hℓ : 2 ≤ ℓ) (σ : Vec d) (k : Fin d → ℤ) : (MeasureTheory.volume (coreEnlarge ℓ σ k)).toReal = (3 * ℓ - 2) ^ d

Volume of the closed enlargement, as a real number: (3ℓ − 2)^d.

theorem HCPolySupport.coreCutoff_support_volume_le {d : ℕ} {ℓ : ℝ} (hℓ : 4 ≤ ℓ) (σ : Vec d) (k : Fin d → ℤ) (U : Set (Vec d)) : (MeasureTheory.volume (Function.support (coreCutoff ℓ σ k) ∩ U)).toReal ≤ (3 * ℓ) ^ d

Support-volume bound. (vol (supp η ∩ U)).toReal ≤ (3ℓ)^d for any set U.

noncomputable def HCPolySupport.coreSqGrad {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Vec d → ℝ

The squared gradient, as a function.

Equations

• HCPolySupport.coreSqGrad ℓ σ k x = ∑ i : Fin d, (fderiv ℝ (HCPolySupport.coreCutoff ℓ σ k) x) (HCPolySupport.basisVec i) ^ 2

theorem HCPolySupport.coreSqGrad_nonneg {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) (x : Vec d) : 0 ≤ coreSqGrad ℓ σ k x

theorem HCPolySupport.continuous_coreSqGrad {d : ℕ} (ℓ : ℝ) (σ : Vec d) (k : Fin d → ℤ) : Continuous (coreSqGrad ℓ σ k)

theorem HCPolySupport.integrable_coreSqGrad {d : ℕ} {ℓ : ℝ} (hℓ : 4 ≤ ℓ) (σ : Vec d) (k : Fin d → ℤ) : MeasureTheory.Integrable (coreSqGrad ℓ σ k) MeasureTheory.volume

The squared gradient is supported in the closed enlargement, hence globally integrable.

theorem HCPolySupport.coreCutoff_sqGrad_integral_le {d : ℕ} {ℓ : ℝ} (hℓ : 4 ≤ ℓ) (σ : Vec d) (k : Fin d → ℤ) (U : Set (Vec d)) : ∫ (x : Vec d) in U, ∑ i : Fin d, (fderiv ℝ (coreCutoff ℓ σ k) x) (basisVec i) ^ 2 ≤ ↑d * (16 / ℓ) ^ 2 * (3 * ℓ) ^ d

Squared-gradient integral bound. ∫_U Σᵢ (∂ᵢ η)² ≤ d · (16/ℓ)² · (3ℓ)^d.