Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.W1p.H10GradientUpgrade

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

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

Upgrading zero-trace H¹ witnesses from finite-p gradients #

An H¹₀ witness whose weak gradient has finite L^p control belongs to W^{1,p}_0 on every bounded open convex domain. The zero-trace approximation is constructed internally by inwardly mollifying the global zero extension.

source
noncomputable def HCPolySupport.H10Function.inwardApproximation {d : ℕ} {U : Set (Vec d)} (u : H10Function U) (x0 : Vec d) (r : ℝ) (n : ℕ) :
Vec d → ℝ

The zero extension of u mollified at scale r / (n + 1) and evaluated after the outward affine dilation based at x0.

Equations
Instances For
    source
    theorem HCPolySupport.H10Function.inwardApproximation_properties {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) {x0 : Vec d} {r : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (n : ℕ) :
    ContDiff ℝ (↑⊤) (u.inwardApproximation x0 r n) ∧ HasCompactSupport (u.inwardApproximation x0 r n) ∧ tsupport (u.inwardApproximation x0 r n) ⊆ U
    source
    theorem HCPolySupport.H10Function.tendsto_inwardApproximation_value {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hu : MemLpOn U p.exponent u.toFun) (x0 : Vec d) {r : ℝ} (hr : 0 < r) :
    Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => u.inwardApproximation x0 r n x - u.toFun x) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
    source
    theorem HCPolySupport.H10Function.tendsto_inwardApproximation_grad {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) (x0 : Vec d) {r : ℝ} (hr : 0 < r) (i : Fin d) :
    Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (u.inwardApproximation x0 r n) x) (basisVec i) - u.grad x i) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)
    source
    noncomputable def HCPolySupport.H10Function.toW10pOfGradMemLpNonempty {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) (hU_nonempty : U.Nonempty) :
    W10pFunction U p.exponent

    Upgrade of a zero-trace H¹ function with Lᵖ gradient to W^{1,p}_0 on a nonempty bounded open convex domain, using inward smooth approximations.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.H10Function.toW10pOfGradMemLpEmpty {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) (hU_empty : U = ∅) :
      W10pFunction U p.exponent

      Upgrade of a zero-trace H¹ function with Lᵖ gradient to W^{1,p}_0 on the empty domain, using zero smooth approximations.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.H10Function.toW10pOfGradMemLp {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) :
        W10pFunction U p.exponent

        Upgrade an H¹₀ witness on a bounded open convex domain to W^{1,p}_0 when its weak-gradient coordinates have finite L^p control. Both the function and weak-gradient representatives are preserved exactly.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem HCPolySupport.H10Function.toW10pOfGradMemLp_toFun {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) :
          (toW10pOfGradMemLp hU u p hgrad).toFun = u.toFun
          source
          @[simp]
          theorem HCPolySupport.H10Function.toW10pOfGradMemLp_grad {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H10Function U) (p : FiniteLpExponent) (hgrad : GradMemLpOn U p.exponent u.grad) :
          (toW10pOfGradMemLp hU u p hgrad).grad = u.grad