Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.H1.LocalizedZeroTrace

Coarse-graining support: Support.Sobolev.H1.LocalizedZeroTrace #

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

source
def HCPolySupport.LocalizedZeroTraceFunctionOn {d : ℕ} (Ω V : Set (Vec d)) (u : Vec d → ℝ) :
Prop

Localized scalar zero-trace condition.

This is the Sobolev/a.e. replacement for saying that a scalar function vanishes on the part of ∂Ω seen through the localization window V: every smooth compactly supported cutoff localized in V turns the function into an admissible H¹₀(Ω) test function.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.localizedZeroTraceFunctionOn_memH10_mul {d : ℕ} {Ω V : Set (Vec d)} {u η : Vec d → ℝ} (hu : LocalizedZeroTraceFunctionOn Ω V u) (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ V) :
    MemH10 Ω fun (y : Vec d) => η y * u y

    The localized scalar zero-trace condition gives exactly the admissible cutoff product encoded in its definition.

    source
    theorem HCPolySupport.localizedZeroTraceFunctionOn_of_h10 {d : ℕ} {Ω V : Set (Vec d)} (hΩ : IsOpen Ω) (hV : V ⊆ Ω) (u : H10Function Ω) :
    LocalizedZeroTraceFunctionOn Ω V u.toFun

    A genuine H¹₀(Ω) function has localized zero trace in every window contained in Ω.

    source
    theorem HCPolySupport.localizedZeroTraceFunctionOn_of_h10_any {d : ℕ} {Ω V : Set (Vec d)} (u : H10Function Ω) :
    LocalizedZeroTraceFunctionOn Ω V u.toFun

    A genuine H¹₀(Ω) function has localized zero trace in any localization window. The cutoff need not be supported in Ω: the compactly supported approximants of the H¹₀ function are already supported in Ω.

    source
    theorem HCPolySupport.localizedZeroTraceFunctionOn_add {d : ℕ} {Ω V : Set (Vec d)} {u v : Vec d → ℝ} (hu : LocalizedZeroTraceFunctionOn Ω V u) (hv : LocalizedZeroTraceFunctionOn Ω V v) :
    LocalizedZeroTraceFunctionOn Ω V fun (y : Vec d) => u y + v y

    Localized zero trace is closed under addition.

    source
    theorem HCPolySupport.localizedZeroTraceFunctionOn_neg {d : ℕ} {Ω V : Set (Vec d)} {u : Vec d → ℝ} (hu : LocalizedZeroTraceFunctionOn Ω V u) :
    LocalizedZeroTraceFunctionOn Ω V fun (y : Vec d) => -u y

    Localized zero trace is closed under negation.

    source
    theorem HCPolySupport.localizedZeroTraceFunctionOn_sub {d : ℕ} {Ω V : Set (Vec d)} {u v : Vec d → ℝ} (hu : LocalizedZeroTraceFunctionOn Ω V u) (hv : LocalizedZeroTraceFunctionOn Ω V v) :
    LocalizedZeroTraceFunctionOn Ω V fun (y : Vec d) => u y - v y

    Localized zero trace is closed under subtraction.