Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.PublicTheorems

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

theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositive (d : ℕ) : CubeKBesovPartialBoundByOverlappingPositive d

Pure/K-interface analytic input: finite-level K-functional partial sums are controlled by the overlapping positive partial sums and mean term.

This is proved by the concrete smooth overlap averaging operator and the K-functional depth/partial assembly.

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

Uniform pure/K-interface input: finite-level K-functional partial sums are controlled by the overlapping positive partial sums and mean term with a dimension-only constant, independent of s.

theorem HCPolySupport.cubeKBesovInputBoundednessOfOverlappingHRegularity (d : ℕ) : CubeKBesovInputBoundednessOfOverlappingHRegularity d

Pure/K-interface analytic input: overlapping Besov regularity gives bounded canonical K-functional partial sums.

theorem HCPolySupport.cubeDirichletGradientAverageRegularity (d : ℕ) [NeZero d] : CubeDirichletGradientAverageRegularity d

Mean-term estimate for zero-Dirichlet divergence solutions. This is proved by transporting the open-cube zero-trace function to the half-open cube used by cubeAverageVec, then applying the zero-trace averaged-gradient identity.

theorem HCPolySupport.cubeDirichletDivergenceEnergyEstimate (d : ℕ) : CubeDirichletDivergenceEnergyEstimate d

PDE endpoint estimate: one-solution L² energy estimate for zero-Dirichlet divergence solutions. This is the formal test-with-the-solution argument.

theorem HCPolySupport.cubeDirichletDivergenceResidualL2Stability (d : ℕ) : CubeDirichletDivergenceResidualL2Stability d

Residual L² stability is a theorem once the one-solution energy estimate is available: subtract the two weak equations, then apply the estimate to the residual solution.

noncomputable def HCPolySupport.identityCoeffField (d : ℕ) : CoeffField d

The identity coefficient field, represented as the scalar matrix 1 • I.

Equations

• HCPolySupport.identityCoeffField d x✝ = HCPolySupport.scalarMatrix 1

theorem HCPolySupport.matVecMul_identityCoeffField {d : ℕ} (x ξ : Vec d) : matVecMul (identityCoeffField d x) ξ = ξ

theorem HCPolySupport.isEllipticFieldOn_identityCoeffField {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) : IsEllipticFieldOn 1 1 U (identityCoeffField d)

theorem HCPolySupport.openCubeSet_nonempty_internal {d : ℕ} (Q : TriadicCube d) : (openCubeSet Q).Nonempty

theorem HCPolySupport.cubeVectorH1DivergencePoissonRealization (d : ℕ) [NeZero d] : CubeVectorH1DivergencePoissonRealization d

PDE endpoint analytic input: weak-divergence realization for coordinatewise H¹ vector fields. The scalar Dirichlet H² estimate is already proved, so this is now the remaining bridge from vector divergence data to scalar Poisson forcing.

theorem HCPolySupport.cubeDirichletDivergenceH2CompetitorRegularity (d : ℕ) [NeZero d] : CubeDirichletDivergenceH2CompetitorRegularity d

Dirichlet H² regularity for divergence RHS generated by an H¹ vector competitor, assembled from the scalar H² theorem and the weak-divergence realization bridge.

theorem HCPolySupport.cubeDirichletH1CompetitorLiftRegularity (d : ℕ) [NeZero d] : CubeDirichletH1CompetitorLiftRegularity d

Dirichlet H² regularity as an H¹ solution-gradient lift for each H¹ vector competitor, assembled from the sharper divergence-H² contract.

theorem HCPolySupport.cubeDirichletKEndpointCompetitorConstruction (d : ℕ) [NeZero d] : CubeDirichletKEndpointCompetitorConstruction d

Two-constant endpoint construction assembled from residual L² stability and the Dirichlet H² competitor lift.

theorem HCPolySupport.cubeDirichletKEndpointDecomposition (d : ℕ) [NeZero d] : CubeDirichletKEndpointDecomposition d

One-constant endpoint decomposition assembled from the two endpoint constants.

theorem HCPolySupport.cubeKFunctionalDirichletPointwiseRegularity (d : ℕ) [NeZero d] : CubeKFunctionalDirichletPointwiseRegularity d

Pointwise K-functional regularity assembled from the endpoint decomposition.

theorem HCPolySupport.discreteConstantCoefficientDirichletBesovFunctionSpaces_of_partialBoundByOverlappingPositive {d : ℕ} [NeZero d] (hpartial : CubeKBesovPartialBoundByOverlappingPositive d) : DiscreteConstantCoefficientDirichletBesovFunctionSpaces d

Direct assembly of the discrete compatibility Dirichlet Besov statement from the finite-level pure K/overlapping comparison. This is not the source theorem pending the continuum K/H^s gate.

This avoids using the over-strong all-functions K/overlapping equivalence package. The output overlap norm is controlled by the proved overlap-Poincare comparison and bounded K partial sums for the output; those bounded output partials come from pointwise K-regularity and the input boundedness supplied by the finite-level partial comparison.

theorem HCPolySupport.cubeKBesovDirichletRegularityComponents (d : ℕ) [NeZero d] : CubeKBesovDirichletRegularityComponents d

Focused components for the PDE/K-functional part of the revised proof.

theorem HCPolySupport.cubeKBesovDirichletRegularity (d : ℕ) [NeZero d] : CubeKBesovDirichletRegularity (cubeKBesovNormModel d)

PDE/K-functional regularity assembled from the three focused analytic inputs.

theorem HCPolySupport.exists_cubeKBesovDirichletRegularityUniform (d : ℕ) [NeZero d] : ∃ (C : ℝ), CubeKBesovDirichletRegularityUniform (cubeKBesovNormModel d) C

Uniform-in-s PDE/K-functional regularity.

theorem HCPolySupport.exists_discreteConstantCoefficientDirichletBesovFunctionSpacesUniform (d : ℕ) [NeZero d] : ∃ (C : ℝ), DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform d C

Uniform discrete compatibility theorem, with one dimension-only constant for all s ∈ (0,1). It is not the source theorem pending the continuum K/H^s gate.

theorem HCPolySupport.discreteConstantCoefficientDirichletBesovFunctionSpaces (d : ℕ) [NeZero d] : DiscreteConstantCoefficientDirichletBesovFunctionSpaces d

Discrete compatibility theorem assembled from the direct finite-partial K/overlapping route. It is not the source theorem pending the continuum K/H^s gate.