Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.ConstantCoefficientDirichletBesov.ConcreteAveraging

Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.ConcreteAveraging #

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

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

Residual constant for the concrete smooth overlap averaging operator.

Equations
Instances For
    source
    theorem HCPolySupport.concreteOverlapAveragingResidualConstant_nonneg (d : ℕ) :
    0 ≤ concreteOverlapAveragingResidualConstant d
    source
    noncomputable def HCPolySupport.concreteOverlapAveragingGradientConstant (d : ℕ) :
    ℝ

    Gradient constant for the concrete smooth overlap averaging operator.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.concreteOverlapAveragingGradientConstant_nonneg (d : ℕ) :
      0 ≤ concreteOverlapAveragingGradientConstant d
      source
      noncomputable def HCPolySupport.concreteOverlapAveragingCompetitorConstant (d : ℕ) :
      ℝ

      Dimension-only constant controlling both the residual and the scaled gradient of the concrete smooth overlap averaging competitor.

      Equations
      Instances For
        source
        theorem HCPolySupport.concreteOverlapAveragingCompetitorConstant_nonneg (d : ℕ) :
        0 ≤ concreteOverlapAveragingCompetitorConstant d
        source
        theorem HCPolySupport.concreteSmoothOverlapPartition_residualConstant {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
        (concreteSmoothOverlapPartition Q j).residualConstant = concreteOverlapAveragingResidualConstant d
        source
        theorem HCPolySupport.concreteSmoothOverlapPartition_gradientConstant {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
        (concreteSmoothOverlapPartition Q j).gradientConstant = concreteOverlapAveragingGradientConstant d
        source
        theorem HCPolySupport.concreteSmoothOverlapPartition_residualConstant_le_competitorConstant {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
        (concreteSmoothOverlapPartition Q j).residualConstant ≤ concreteOverlapAveragingCompetitorConstant d
        source
        theorem HCPolySupport.concreteSmoothOverlapPartition_gradientConstant_le_competitorConstant {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
        (concreteSmoothOverlapPartition Q j).gradientConstant ≤ concreteOverlapAveragingCompetitorConstant d
        source
        theorem HCPolySupport.cubeKBesovOverlapAveragingCompetitorEstimate_concrete (d : ℕ) :
        CubeKBesovOverlapAveragingCompetitorEstimate d (concreteOverlapAveragingCompetitorConstant d)

        The concrete normalized smooth overlap partition supplies the one-depth averaging competitor estimate with a dimension-only constant.

        source
        theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositiveUniform_concrete (d : ℕ) :
        CubeKBesovPartialBoundByOverlappingPositiveUniform d (2 * concreteOverlapAveragingCompetitorConstant d)

        Concrete replacement for the finite-level K/overlapping comparison input used by the public constant-coefficient Dirichlet Besov theorem.

        source
        theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositive_concrete (d : ℕ) :
        CubeKBesovPartialBoundByOverlappingPositive d

        Concrete replacement for the finite-level K/overlapping comparison input used by the public constant-coefficient Dirichlet Besov theorem.