Documentation

LeanPool.HighContrastHomogenization.Support.HighContrast.Coupled.LocalEnergy.Cutoff

Coarse-graining support: Support.HighContrast.Coupled.LocalEnergy.Cutoff #

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

Local block energy: the squared cutoff η² #

Smoothness, [0,1]-bounds, and the product-rule gradient ∂ᵢ(η²) = 2 η ∂ᵢη for the squared cutoff, together with the L^∞ memberships (on a finite-measure domain) needed to feed the library's smooth×H¹ product constructions.

source
def HCPolySupport.sqCutoff {d : ℕ} (η : Vec d → ℝ) :
Vec d → ℝ

The squared cutoff.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.sqCutoff_apply {d : ℕ} (η : Vec d → ℝ) (x : Vec d) :
    sqCutoff η x = η x ^ 2
    source
    theorem HCPolySupport.sqCutoff_contDiff {d : ℕ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) :
    ContDiff ℝ (↑⊤) (sqCutoff η)
    source
    theorem HCPolySupport.sqCutoff_nonneg {d : ℕ} (η : Vec d → ℝ) (x : Vec d) :
    0 ≤ sqCutoff η x
    source
    theorem HCPolySupport.sqCutoff_le_one {d : ℕ} {η : Vec d → ℝ} (hη : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (x : Vec d) :
    sqCutoff η x ≤ 1
    source
    theorem HCPolySupport.abs_sqCutoff_le_one {d : ℕ} {η : Vec d → ℝ} (hη : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (x : Vec d) :
    |sqCutoff η x| ≤ 1
    source
    theorem HCPolySupport.fderiv_sqCutoff {d : ℕ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (x : Vec d) (i : Fin d) :
    (fderiv ℝ (sqCutoff η) x) (basisVec i) = 2 * η x * (fderiv ℝ η x) (basisVec i)

    The product-rule gradient of η²: ∂ᵢ(η²) = 2 η ∂ᵢη.

    source
    theorem HCPolySupport.support_sqCutoff {d : ℕ} (η : Vec d → ℝ) :
    Function.support (sqCutoff η) = Function.support η

    The support of η² equals the support of η.

    L^∞ memberships on a finite-measure domain #

    source
    theorem HCPolySupport.memLpTop_sqCutoff {d : ℕ} {U : Set (Vec d)} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) :
    MeasureTheory.MemLp (sqCutoff η) ⊤ (MeasureTheory.volume.restrict U)
    source
    theorem HCPolySupport.memLpTop_fderiv_sqCutoff {d : ℕ} {U : Set (Vec d)} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) {Gη : ℝ} (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (i : Fin d) :
    MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ (sqCutoff η) x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)