Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeDirichletH2.Definitions

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

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

Cube Dirichlet H² regularity interfaces #

This file freezes the theorem surface for the cube Dirichlet H² endpoint needed by the Chapter 1 Hodge projection argument. The analytic proof is planned as an odd-reflection sibling of the existing Neumann/CZ reflection endpoint; this file contains only the stable problem and regularity contracts.

source
def HCPolySupport.CubeDirichletWeakPoissonProblem {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) (f : Vec d → ℝ) :
Prop

Scalar weak Dirichlet Poisson problem on a cube.

The sign convention is -Delta u = f, encoded by int_Q grad u . grad phi = int_Q f phi for all zero-trace tests.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HCPolySupport.CubeDirichletH2Regularity {d : ℕ} (Q : TriadicCube d) (C : ℝ) :
    Prop

    Cube Dirichlet H² regularity in the repository's weak-Hessian form.

    The Hessian size is measured by HasWeakHessianOn.hessianCoordL2NormSum, the same quantity used by the existing Neumann/CZ endpoint. The forcing norm is the normalized cube L² norm, matching the positive Besov/CZ layer.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def HCPolySupport.CubeDirichletH2RegularityInDimension (d : ℕ) (C : ℝ) :
      Prop

      Dimension-uniform cube Dirichlet H² regularity.

      Equations
      Instances For
        source
        def HCPolySupport.CubeDirichletH2RegularityVolumeL2 {d : ℕ} (Q : TriadicCube d) (C : ℝ) :
        Prop

        Cube Dirichlet H² regularity with the unnormalized open-cube L² forcing norm on the right-hand side. The input integrability is still phrased for the normalized cube measure so this contract can be consumed by the same Besov/CZ callers as CubeDirichletH2Regularity.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def HCPolySupport.CubeDirichletH2RegularityVolumeL2InDimension (d : ℕ) (C : ℝ) :
          Prop

          Dimension-uniform cube Dirichlet H² regularity with the unnormalized open-cube L² forcing norm.

          Equations
          Instances For
            source
            theorem HCPolySupport.CubeDirichletH2Regularity.constant_nonneg {d : ℕ} {Q : TriadicCube d} {C : ℝ} (h : CubeDirichletH2Regularity Q C) :
            0 ≤ C
            source
            theorem HCPolySupport.CubeDirichletH2RegularityInDimension.constant_nonneg {d : ℕ} {C : ℝ} (h : CubeDirichletH2RegularityInDimension d C) :
            0 ≤ C
            source
            theorem HCPolySupport.CubeDirichletH2RegularityVolumeL2.constant_nonneg {d : ℕ} {Q : TriadicCube d} {C : ℝ} (h : CubeDirichletH2RegularityVolumeL2 Q C) :
            0 ≤ C
            source
            theorem HCPolySupport.CubeDirichletH2RegularityVolumeL2InDimension.constant_nonneg {d : ℕ} {C : ℝ} (h : CubeDirichletH2RegularityVolumeL2InDimension d C) :
            0 ≤ C
            source
            theorem HCPolySupport.CubeDirichletH2Regularity.mono {d : ℕ} {Q : TriadicCube d} {C D : ℝ} (h : CubeDirichletH2Regularity Q C) (hCD : C ≤ D) :
            CubeDirichletH2Regularity Q D

            The local Dirichlet H² regularity estimate may be enlarged to any larger constant.

            source
            theorem HCPolySupport.CubeDirichletH2RegularityInDimension.mono {d : ℕ} {C D : ℝ} (h : CubeDirichletH2RegularityInDimension d C) (hCD : C ≤ D) :
            CubeDirichletH2RegularityInDimension d D

            The dimension-uniform Dirichlet H² regularity estimate may be enlarged to any larger constant.

            source
            theorem HCPolySupport.CubeDirichletH2RegularityVolumeL2.mono {d : ℕ} {Q : TriadicCube d} {C D : ℝ} (h : CubeDirichletH2RegularityVolumeL2 Q C) (hCD : C ≤ D) :
            CubeDirichletH2RegularityVolumeL2 Q D

            The unnormalized local Dirichlet H² regularity estimate may be enlarged to any larger constant.

            source
            theorem HCPolySupport.CubeDirichletH2RegularityVolumeL2InDimension.mono {d : ℕ} {C D : ℝ} (h : CubeDirichletH2RegularityVolumeL2InDimension d C) (hCD : C ≤ D) :
            CubeDirichletH2RegularityVolumeL2InDimension d D

            The dimension-uniform unnormalized Dirichlet H² regularity estimate may be enlarged to any larger constant.