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

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

theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositive_of_depthBound {d : ℕ} (hdepth : CubeKBesovDepthBoundByOverlappingPositive d) : CubeKBesovPartialBoundByOverlappingPositive d

The depthwise smoothing estimate implies the exact finite partial bound used by the public Dirichlet Besov theorem. The mean term in the public statement is harmless here; the depthwise estimate controls the K-partial seminorm directly by the overlapping partial seminorm.

theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositiveUniform_of_depthBound {d : ℕ} {C : ℝ} (hdepth : CubeKBesovDepthBoundByOverlappingPositiveUniform d C) : CubeKBesovPartialBoundByOverlappingPositiveUniform d C

Uniform-in-s depth control implies the uniform finite partial K/overlap comparison.

theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositive_of_overlapAveragingCompetitorEstimate {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hcomp : CubeKBesovOverlapAveragingCompetitorEstimate d C) : CubeKBesovPartialBoundByOverlappingPositive d

Direct Phase-7 bridge: the one-depth overlap-averaging competitor estimate is enough to replace the finite partial K/overlap axiom.

theorem HCPolySupport.cubeKBesovPartialBoundByOverlappingPositiveUniform_of_overlapAveragingCompetitorEstimate {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hcomp : CubeKBesovOverlapAveragingCompetitorEstimate d C) : CubeKBesovPartialBoundByOverlappingPositiveUniform d (2 * C)

Uniform version of the Phase-7 bridge from the concrete overlap averaging competitor estimate to the finite partial K/overlap comparison.

theorem HCPolySupport.cubeKBesovInputBoundednessOfOverlappingHRegularity_of_partialBoundByOverlappingPositive {d : ℕ} (hpartial : CubeKBesovPartialBoundByOverlappingPositive d) : CubeKBesovInputBoundednessOfOverlappingHRegularity d

The finite-level K/overlapping comparison implies the boundedness bridge needed to use the full K-functional seminorm for overlapping-regular inputs.

theorem HCPolySupport.overlappingPositiveSeminorm_le_KSeminorm_of_overlapPoincare {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hPoincare : CubeVectorH1OverlapPoincareEstimate d C) (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hK_bdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N F)) : cubeBesovOverlappingPositiveVectorSeminormTwo Q s F ≤ (8 * 3 ^ d + 2 * C ^ 2 + 1) * cubeKBesovVectorSeminormTwo Q s F

The proved overlap-Poincare estimate controls the full overlapping positive seminorm by the full K-functional seminorm, provided the K partial seminorms are bounded above so the real sSup is a genuine supremum.

theorem HCPolySupport.cubeVectorOverlappingBesovHRegularity_of_memLp_of_kPartial_bddAbove {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hPoincare : CubeVectorH1OverlapPoincareEstimate d C) (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hK_bdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N F)) : CubeVectorOverlappingBesovHRegularity Q s F

Bounded K-functional partial sums give overlapping Besov regularity.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorNormTwo_le_mul_cubeKBesovVectorNormTwo_of_overlapPoincare {d : ℕ} {C : ℝ} (hC : 0 ≤ C) (hPoincare : CubeVectorH1OverlapPoincareEstimate d C) (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) (hK_bdd : BddAbove (Set.range fun (N : ℕ) => cubeKBesovVectorPartialSeminormTwo Q s N F)) : cubeBesovOverlappingPositiveVectorNormTwo Q s F ≤ (8 * 3 ^ d + 2 * C ^ 2 + 2) * cubeKBesovVectorNormTwo Q s F

Norm-level version of the overlap-to-K comparison. The mean term is the same on both sides, so the seminorm comparison only costs one extra additive constant.

theorem HCPolySupport.cubeKBesovVectorNormTwo_le_mul_cubeBesovOverlappingPositiveVectorNormTwo_of_partialBound {d : ℕ} (hpartial : CubeKBesovPartialBoundByOverlappingPositive d) {s : ℝ} (hs_pos : 0 < s) (hs_lt : s < 1) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (Q : TriadicCube d) (F : Vec d → Vec d), CubeVectorOverlappingBesovHRegularity Q s F → cubeKBesovVectorNormTwo Q s F ≤ C * cubeBesovOverlappingPositiveVectorNormTwo Q s F

The finite-level K-partial comparison gives a full K-norm bound on every input with overlapping Besov regularity.

theorem HCPolySupport.cubeKBesovVectorNormTwo_le_mul_cubeBesovOverlappingPositiveVectorNormTwo_of_partialBoundUniform {d : ℕ} {C : ℝ} (hpartial : CubeKBesovPartialBoundByOverlappingPositiveUniform d C) {s : ℝ} (hs_pos : 0 < s) (hs_lt : s < 1) (Q : TriadicCube d) (F : Vec d → Vec d) : CubeVectorOverlappingBesovHRegularity Q s F → cubeKBesovVectorNormTwo Q s F ≤ (C + 1) * cubeBesovOverlappingPositiveVectorNormTwo Q s F

Uniform version of the K-norm bound by the corrected overlapping positive norm.

def HCPolySupport.CubeDirichletGradientAverageRegularity (d : ℕ) : Prop

Mean-term estimate for the gradient of the zero-Dirichlet divergence solution. In the classical proof this is the zero-trace averaged-gradient identity, packaged as an estimate so it composes with the norm algebra.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeKFunctionalDirichletPointwiseRegularity (d : ℕ) : Prop

Pointwise-in-scale K-functional estimate for the zero-Dirichlet divergence solution operator. This is the interpolation core before summing over dyadic/triadic depths.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDirichletKEndpointDecomposition (d : ℕ) : Prop

Endpoint decomposition needed for the K-functional proof. For each H¹ competitor G for the datum h, produce an H¹ competitor V for the solution gradient whose residual is controlled by the L² endpoint and whose H¹ size is controlled by the Dirichlet H² endpoint.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDirichletKEndpointCompetitorConstruction (d : ℕ) : Prop

Two-constant endpoint construction behind CubeDirichletKEndpointDecomposition. The first constant is the L² residual stability constant; the second is the Dirichlet H²/H¹ competitor-size constant. Keeping them separate mirrors the analytic proof before the final K-functional algebra absorbs both into one constant.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDirichletDivergenceEnergyEstimate (d : ℕ) : Prop

One-solution energy estimate for the constant-coefficient zero-Dirichlet divergence solver. This is the real analytic input behind residual stability: test the equation with the solution and apply Cauchy-Schwarz.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDirichletDivergenceResidualL2Stability (d : ℕ) : Prop

Residual L² stability for the constant-coefficient zero-Dirichlet divergence solver. This packages the energy estimate applied to the difference of two solutions, avoiding any commitment here to a particular formalization of solution subtraction.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDirichletH1CompetitorLiftRegularity (d : ℕ) : Prop

Dirichlet H² endpoint as an H¹ lift for vector-field competitors. Given an H¹ vector competitor G, solve the corresponding divergence-RHS Dirichlet problem and realize its gradient as a coordinatewise H¹ vector field V, with the expected H¹ bound.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeVectorH1DivergencePoissonRealization (d : ℕ) : Prop

Weak-divergence realization needed to feed the scalar Dirichlet H² theorem. For each coordinatewise H¹ vector field G, the zero-Dirichlet solution of the divergence problem is also a scalar Poisson solution with forcing div G.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeDirichletDivergenceH2CompetitorRegularity (d : ℕ) : Prop

Sharper analytic form of the Dirichlet H² endpoint for H¹ vector competitors. It supplies the divergence-RHS solution and a weak Hessian bound; the coordinatewise H¹ competitor is then a formal wrapper around the Hessian witness.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeDirichletDivergenceH2CompetitorRegularity_of_vectorH1DivergencePoissonRealization {d : ℕ} [NeZero d] (hreal : CubeVectorH1DivergencePoissonRealization d) : CubeDirichletDivergenceH2CompetitorRegularity d

theorem HCPolySupport.cubeDirichletH1CompetitorLiftRegularity_of_divergenceH2CompetitorRegularity {d : ℕ} (hH2 : CubeDirichletDivergenceH2CompetitorRegularity d) : CubeDirichletH1CompetitorLiftRegularity d

theorem HCPolySupport.cubeDirichletDivergenceProblem_sub {d : ℕ} {Q : TriadicCube d} {h k : Vec d → Vec d} {w v : H10Function (openCubeSet Q)} (hh : MeasureTheory.MemLp h 2 (normalizedCubeMeasure Q)) (hk : MeasureTheory.MemLp k 2 (normalizedCubeMeasure Q)) (hw : CubeDirichletDivergenceProblem Q w h) (hv : CubeDirichletDivergenceProblem Q v k) : CubeDirichletDivergenceProblem Q (w - v) fun (x : Vec d) => h x - k x

theorem HCPolySupport.cubeDirichletDivergenceResidualL2Stability_of_energyEstimate {d : ℕ} (henergy : CubeDirichletDivergenceEnergyEstimate d) : CubeDirichletDivergenceResidualL2Stability d

theorem HCPolySupport.cubeDirichletKEndpointCompetitorConstruction_of_residualStability_of_liftRegularity {d : ℕ} (hstable : CubeDirichletDivergenceResidualL2Stability d) (hlift : CubeDirichletH1CompetitorLiftRegularity d) : CubeDirichletKEndpointCompetitorConstruction d

theorem HCPolySupport.cubeDirichletKEndpointDecomposition_of_competitorConstruction {d : ℕ} (hendpoint : CubeDirichletKEndpointCompetitorConstruction d) : CubeDirichletKEndpointDecomposition d

theorem HCPolySupport.cubeKFunctionalDirichletPointwiseRegularity_of_endpointDecomposition {d : ℕ} (hendpoint : CubeDirichletKEndpointDecomposition d) : CubeKFunctionalDirichletPointwiseRegularity d

def HCPolySupport.CubeKBesovDirichletRegularityComponents (d : ℕ) : Prop

The three focused ingredients that imply the K-functional Dirichlet Besov regularity statement.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeKBesovCanonicalOverlappingTheory (d : ℕ) : Prop

The full pure function-space input for the canonical K-functional model: norm equivalence with the corrected overlapping positive Besov norm, together with boundedness of the canonical K partial sums for overlapping-regular inputs.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.CubeKBesovCanonicalOverlappingTheoryCore (d : ℕ) : Prop

Sharpened pure canonical K-functional/overlapping theory. The second component is finite-level K-partial control by the overlapping-positive partial sums, which then implies the boundedness bridge for full K-seminorms.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CubeKBesovCanonicalOverlappingTheoryCore.to_canonicalOverlappingTheory {d : ℕ} (hcore : CubeKBesovCanonicalOverlappingTheoryCore d) : CubeKBesovCanonicalOverlappingTheory d

theorem HCPolySupport.cubeKBesovDirichletRegularity_of_components {d : ℕ} (hcomponents : CubeKBesovDirichletRegularityComponents d) : CubeKBesovDirichletRegularity (cubeKBesovNormModel d)

theorem HCPolySupport.exists_cubeKBesovDirichletRegularityUniform_of_components {d : ℕ} (hcomponents : CubeKBesovDirichletRegularityComponents d) : ∃ (C : ℝ), CubeKBesovDirichletRegularityUniform (cubeKBesovNormModel d) C

Uniform-in-s version of the PDE/K-functional regularity assembled from the same three focused components.

def HCPolySupport.DiscreteConstantCoefficientDirichletBesovKFunctionalRoute (d : ℕ) : Prop

Discrete compatibility K-functional route: one pure norm-equivalence input and one PDE/K-functional regularity input. This is not the source theorem pending the continuum K/H^s gate.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.DiscreteConstantCoefficientDirichletBesovFunctionSpaces (d : ℕ) : Prop

Discrete compatibility statement obtained from the finite-level K-functional/overlap machinery. It is not the source theorem l.constant.coefficient.Dirichlet.Besov.function.spaces pending the continuum K/H^s gate.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform (d : ℕ) (C : ℝ) : Prop

Uniform-in-s discrete compatibility strengthening of DiscreteConstantCoefficientDirichletBesovFunctionSpaces, used by the compatibility duality route. It is not the source theorem pending the continuum K/H^s gate.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform.to_functionSpaces {d : ℕ} {C : ℝ} (h : DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform d C) : DiscreteConstantCoefficientDirichletBesovFunctionSpaces d

theorem HCPolySupport.discreteConstantCoefficientDirichletBesovFunctionSpaces_of_discreteKFunctionalRoute {d : ℕ} (hroute : DiscreteConstantCoefficientDirichletBesovKFunctionalRoute d) : DiscreteConstantCoefficientDirichletBesovFunctionSpaces d

Assemble the discrete compatibility Dirichlet Besov statement from the discrete K-functional route.

theorem HCPolySupport.exists_of_partialBoundByOverlappingPositiveUniform {d : ℕ} {Cpartial : ℝ} (hpartial : CubeKBesovPartialBoundByOverlappingPositiveUniform d Cpartial) (hcomponents : CubeKBesovDirichletRegularityComponents d) : ∃ (C : ℝ), DiscreteConstantCoefficientDirichletBesovFunctionSpacesUniform d C

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