Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.W1p.ZeroExtensionGraph

Coarse-graining support: Support.Sobolev.W1p.ZeroExtensionGraph #

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

Zero extension of the H¹₀ graph #

This file realizes the supported smooth approximation built into an H10Function as a global weak-gradient graph: both the value and gradient are extended by zero outside the original domain. The argument uses the given H¹₀ approximants and finite-exponent graph closure, without any cube, trace, dilation, or PDE input.

source
noncomputable def HCPolySupport.H10Function.zeroExtension {d : ℕ} {U : Set (Vec d)} (u : H10Function U) :
Vec d → ℝ

The literal zero extension of the value representative of an H¹₀ function.

Equations
Instances For
    source
    noncomputable def HCPolySupport.H10Function.zeroExtensionGrad {d : ℕ} {U : Set (Vec d)} (u : H10Function U) :
    Vec d → Vec d

    The literal zero extension of the gradient representative of an H¹₀ function.

    Equations
    Instances For
      source
      @[simp]
      theorem HCPolySupport.H10Function.zeroExtension_apply_of_mem {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {x : Vec d} (hx : x ∈ U) :
      u.zeroExtension x = u.toFun x
      source
      @[simp]
      theorem HCPolySupport.H10Function.zeroExtension_apply_of_not_mem {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {x : Vec d} (hx : x ∉ U) :
      u.zeroExtension x = 0
      source
      @[simp]
      theorem HCPolySupport.H10Function.zeroExtensionGrad_apply_of_mem {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {x : Vec d} (hx : x ∈ U) :
      u.zeroExtensionGrad x = u.grad x
      source
      @[simp]
      theorem HCPolySupport.H10Function.zeroExtensionGrad_apply_of_not_mem {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {x : Vec d} (hx : x ∉ U) :
      u.zeroExtensionGrad x = 0
      source
      theorem HCPolySupport.H10Function.memLp_zeroExtension {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {p : ENNReal} (hU : MeasurableSet U) (hu : MeasureTheory.MemLp u.toFun p (MeasureTheory.volume.restrict U)) :
      MeasureTheory.MemLp u.zeroExtension p MeasureTheory.volume

      Restricted L^p membership transports exactly to the global zero extension.

      source
      theorem HCPolySupport.H10Function.gradMemLp_zeroExtensionGrad {d : ℕ} {U : Set (Vec d)} (u : H10Function U) {p : ENNReal} (hU : MeasurableSet U) (hDu : GradMemLpOn U p u.grad) :
      GradMemLpOn Set.univ p u.zeroExtensionGrad

      Restricted coordinatewise L^p membership transports exactly to the global zero-extended gradient.

      source
      theorem HCPolySupport.H10Function.approx_sub_zeroExtension_eq_indicator_sub_zeroExtensionGraph {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (n : ℕ) :
      (fun (x : Vec d) => u.approx n x - u.zeroExtension x) = U.indicator fun (x : Vec d) => u.approx n x - u.toFun x
      source
      theorem HCPolySupport.H10Function.fderiv_approx_sub_zeroExtensionGrad_eq_indicator_sub {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (n : ℕ) (i : Fin d) :
      (fun (x : Vec d) => (fderiv ℝ (u.approx n) x) (basisVec i) - u.zeroExtensionGrad x i) = U.indicator fun (x : Vec d) => (fderiv ℝ (u.approx n) x) (basisVec i) - u.grad x i
      source
      theorem HCPolySupport.H10Function.hasWeakGradientOn_univ_zeroExtension {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (hU : MeasurableSet U) :
      HasWeakGradientOn Set.univ u.zeroExtension u.zeroExtensionGrad

      The literal zero extensions of an H¹₀ value and gradient form a global weak-gradient graph.

      source
      noncomputable def HCPolySupport.H10Function.extendByZeroToOpenSuperset {d : ℕ} {U V : Set (Vec d)} (u : H10Function U) (hU : MeasurableSet U) (hV : IsOpen V) (hUV : U ⊆ V) :
      H10Function V

      An H¹₀ function on a measurable set is canonically transported to every open superset by its literal zero extension.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HCPolySupport.H10Function.extendByZeroToOpenSuperset_toFun {d : ℕ} {U V : Set (Vec d)} (u : H10Function U) (hU : MeasurableSet U) (hV : IsOpen V) (hUV : U ⊆ V) :
        (u.extendByZeroToOpenSuperset hU hV hUV).toFun = u.zeroExtension
        source
        @[simp]
        theorem HCPolySupport.H10Function.extendByZeroToOpenSuperset_grad {d : ℕ} {U V : Set (Vec d)} (u : H10Function U) (hU : MeasurableSet U) (hV : IsOpen V) (hUV : U ⊆ V) :
        (u.extendByZeroToOpenSuperset hU hV hUV).grad = u.zeroExtensionGrad