Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentEnergyFactor

Coarse-graining support: #

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentEnergyFactor

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

source
noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyInside (d : ℕ) (m : ℤ) :
ℝ

The forcing-independent factor under the square root in the reflected Neumann solver bound, using cube volume plus one.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyConstant (d : ℕ) (m : ℤ) :
    ℝ

    The coefficient obtained by factoring the normalized forcing norm out of the reflected-parent solver energy bound.

    Equations
    Instances For
      source
      theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyConstant_nonneg (d : ℕ) (m : ℤ) :
      0 ≤ originCubeParentReducedSolverEnergyConstant d m
      source
      theorem HCPolySupport.MeanZeroNeumannPoissonSolution.originCubeParentReducedSolverEnergyBound_eq_constant_mul_cubeLpNorm (d : ℕ) (m : ℤ) (F : Vec d → ℝ) (i : Fin d) :
      originCubeParentReducedSolverEnergyBound d m F i = originCubeParentReducedSolverEnergyConstant d m * cubeLpNorm (originCube d m) 2 F