Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedParentInteriorHessian

Coarse-graining support: #

Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedParentInteriorHessian

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

Interior Hessian on an odd-reflected Dirichlet parent #

This internal assembly fixes the geometric radii needed to construct a weak Hessian on the half-scaled parent cube. It retains the exact odd-reflected parent value, gradient, scalar forcing, and weak Poisson equation supplied by the Dirichlet reflection construction.

source
noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.reflectedParentHalfTwoThirdCutoff (d : ℕ) (m : ℤ) :
QuantitativeCubeCutoff (originCube d (m + 1)) (1 / 2) (2 / 3)

Canonical cutoff from the half parent to the two-thirds parent.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.reflectedParentSevenEighthFifteenSixteenthCutoff (d : ℕ) (m : ℤ) :
    QuantitativeCubeCutoff (originCube d (m + 1)) (7 / 8) (15 / 16)

    Canonical outer cutoff leaving a strict margin outside the three-quarter ambient cube.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_cubeDirichletOddReflectionParent_innerHalf_hasWeakHessianOn {d : ℕ} {m : ℤ} {u : H10Function (openCubeSet (originCube d m))} {F : Vec d → ℝ} (hweak : CubeDirichletWeakPoissonProblem (originCube d m) u F) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure (originCube d m))) :
      ∃ (uP : H1Function (openCubeSet (originCube d (m + 1)))), uP.toFun = cubeDirichletOddReflectionScalar (originCube d m) u.toFun ∧ (uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) ∧ WeakPoissonEquationOn (openCubeSet (originCube d (m + 1))) uP (cubeDirichletOddReflectionScalar (originCube d m) F) ∧ ∃ (uS : H1Function (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2))), uS.toFun = uP.toFun ∧ uS.grad = uP.grad ∧ ∃ (H : HasWeakHessianOn (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uS), H.hessianCoordL2NormSum ≤ ∑ i : Fin d, ∑ _j : Fin d, WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound uP (cubeDirichletOddReflectionScalar (originCube d m) F) i (reflectedParentSevenEighthFifteenSixteenthCutoff d m)

      Canonical fixed-radius interior Hessian package for an odd-reflected Dirichlet solution.

      The parent weak equation is returned verbatim. The restricted H¹ function has the same global value and gradient representatives as the parent, and its weak Hessian retains the explicit sum of smooth-test bounds produced by the difference-quotient construction.