Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeDirichletH2.Regularity

Coarse-graining support: Support.Sobolev.Foundations.CubeDirichletH2.Regularity #

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

source
noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2RegularityConstantExact {d : ℕ} [NeZero d] (Q : TriadicCube d) :
ℝ

The scale-indexed Dirichlet H² constant produced by the current zero-trace Poincare/odd-reflection proof.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2RegularityConstantExact_nonneg {d : ℕ} [NeZero d] (Q : TriadicCube d) :
    0 ≤ cubeDirichletH2RegularityConstantExact Q
    source
    noncomputable def HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2VolumeL2Constant (d : ℕ) [NeZero d] :
    ℝ

    The dimension-only constant for the unnormalized open-cube L² forcing version of the Dirichlet H² estimate.

    Equations
    Instances For
      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2VolumeL2Constant_nonneg (d : ℕ) [NeZero d] :
      0 ≤ cubeDirichletH2VolumeL2Constant d
      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2_eq_volumeHalf_mul_volumeL2 {d : ℕ} [NeZero d] (Q : TriadicCube d) :
      cubeDirichletH2RegularityConstantExact Q = cubeVolume Q ^ (1 / 2) * cubeDirichletH2VolumeL2Constant d
      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.originCube_sum_reducedSolverEnergyBoundExact_le_regularityConstant_mul_cubeLpNorm {d : ℕ} [NeZero d] {m : ℤ} {F : Vec d → ℝ} :
      ∑ i : Fin d, ∑ _j : Fin d, originCubeParentReducedSolverEnergyBoundExact d m F i ≤ cubeDirichletH2RegularityConstantExact (originCube d m) * cubeLpNorm (originCube d m) 2 F
      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2RegularityExact {d : ℕ} [NeZero d] (Q : TriadicCube d) :
      CubeDirichletH2Regularity Q (cubeDirichletH2RegularityConstantExact Q)

      Scale-indexed cube Dirichlet H² regularity obtained from odd reflection, the parent-cube interior estimate, and the chosen zero-trace Poincare constant.

      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.cubeDirichletH2RegularityVolumeL2Exact {d : ℕ} [NeZero d] (Q : TriadicCube d) :
      CubeDirichletH2RegularityVolumeL2 Q (cubeDirichletH2VolumeL2Constant d)

      Dimension-only cube Dirichlet H² regularity when the forcing is measured in the unnormalized open-cube L² norm.

      source
      theorem HCPolySupport.CubeDirichletWeakPoissonProblem.exists_cubeDirichletH2RegularityVolumeL2InDimension (d : ℕ) [NeZero d] :
      ∃ (C : ℝ), CubeDirichletH2RegularityVolumeL2InDimension d C

      There exists a dimension-only constant for the unnormalized open-cube L² Dirichlet H² estimate.