Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeBesovPoincare.W12LocalPoincare

Coarse-graining support: Support.Sobolev.Foundations.CubeBesovPoincare.W12LocalPoincare #

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

Local normalized W^{1,2} Poincare estimate on triadic cubes #

The overlap-cube H^1 estimate is used only at the middle child of a triadic cube. There its overlap is the original cube, so the estimate has a dimension-only constant and the exact normalized open-cube Sobolev carrier.

source
noncomputable def HCPolySupport.cubeBesovW12LocalPoincareConstant (d : ℕ) :
ℝ

The dimension-only constant in the local normalized cube Poincare estimate.

Equations
Instances For
    source
    theorem HCPolySupport.cubeBesovW12LocalPoincareConstant_nonneg (d : ℕ) :
    0 ≤ cubeBesovW12LocalPoincareConstant d
    source
    def HCPolySupport.W1pFunction.toH1AtTwo {d : ℕ} {U : Set (Vec d)} (u : W1pFunction U 2) :
    H1Function U

    View a W¹,² function as an H¹ function with the same value and weak gradient.

    Equations
    • u.toH1AtTwo = { toFun := u.toFun, grad := u.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }
    Instances For
      source
      def HCPolySupport.castH1Domain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) :
      H1Function V

      Transport an H¹ function across equality of domains, preserving its value and weak gradient.

      Equations
      Instances For
        source
        theorem HCPolySupport.cubeBesovOscillation_two_le_cubeScaleFactor_mul_normalizedW1pSeminorm {d : ℕ} (Q : TriadicCube d) (u : W1pFunction (openCubeSet Q) 2) :
        cubeBesovOscillation Q 2 u.toFun ≤ cubeBesovW12LocalPoincareConstant d * cubeScaleFactor Q * BoundedMeasurableDomain.NormalizedW1pKernel.seminorm (⋯.toBoundedMeasurableDomain ⋯) 2 cubeBesovOscillation_two_le_cubeScaleFactor_mul_normalizedW1pSeminorm._proof_1 cubeBesovOscillation_two_le_cubeScaleFactor_mul_normalizedW1pSeminorm._proof_2 u

        The local Poincare estimate on a triadic cube in the exact normalized W^{1,2} carrier used by the Besov embedding.