Coarse-graining support:

Support.Sobolev.Fractional.ContinuousInterpolation.ContinuousDiscreteKBridge

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

Exact continuous-to-discrete unit-cube K-functional bridge

This module identifies the two genuine coordinatewise H¹ competitor spaces on the origin unit cube, and compares their residual and gradient quantities. The resulting inequalities are internal transport facts for the finite-depth continuous interpolation argument.

def HCPolySupport.ContinuousKCompetitor.toCubeVectorH1Function {d : ℕ} (G : ContinuousKCompetitor d) : CubeVectorH1Function (originCube d 0)

Regard a continuous source competitor as an internal cube competitor on the origin unit cube.

Equations

• G.toCubeVectorH1Function = { coord := G.coord }

def HCPolySupport.CubeVectorH1Function.toContinuousKCompetitor {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) : ContinuousKCompetitor d

Regard an internal origin-unit-cube competitor as a continuous source competitor.

Equations

• G.toContinuousKCompetitor = { coord := G.coord }

@[simp]

theorem HCPolySupport.ContinuousKCompetitor.toCubeVectorH1Function_coord {d : ℕ} (G : ContinuousKCompetitor d) (i : Fin d) : G.toCubeVectorH1Function.coord i = G.coord i

@[simp]

theorem HCPolySupport.CubeVectorH1Function.toContinuousKCompetitor_coord {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) (i : Fin d) : G.toContinuousKCompetitor.coord i = G.coord i

@[simp]

theorem HCPolySupport.ContinuousKCompetitor.toCubeVectorH1Function_toField {d : ℕ} (G : ContinuousKCompetitor d) : G.toCubeVectorH1Function.toField = G.toField

@[simp]

theorem HCPolySupport.CubeVectorH1Function.toContinuousKCompetitor_toField {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) : G.toContinuousKCompetitor.toField = G.toField

@[simp]

theorem HCPolySupport.ContinuousKCompetitor.toCubeVectorH1Function_grad_apply {d : ℕ} (G : ContinuousKCompetitor d) (x : Vec d) (i j : Fin d) : (G.toCubeVectorH1Function.coord i).grad x j = G.gradient x i j

@[simp]

theorem HCPolySupport.CubeVectorH1Function.toContinuousKCompetitor_gradient_apply {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) (x : Vec d) (i j : Fin d) : G.toContinuousKCompetitor.gradient x i j = (G.coord i).grad x j

@[simp]

theorem HCPolySupport.ContinuousKCompetitor.toCubeVectorH1Function_toContinuousKCompetitor {d : ℕ} (G : ContinuousKCompetitor d) : G.toCubeVectorH1Function.toContinuousKCompetitor = G

@[simp]

theorem HCPolySupport.CubeVectorH1Function.toContinuousKCompetitor_toCubeVectorH1Function {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) : G.toContinuousKCompetitor.toCubeVectorH1Function = G

theorem HCPolySupport.normalizedCubeMeasure_originCube_zero_eq_unitCenteredCubeDomain_normalizedVolume (d : ℕ) : normalizedCubeMeasure (originCube d 0) = (unitCenteredCubeDomain d).normalizedVolume

On the unit cube, the internal cube normalization is exactly the source normalized volume.

theorem HCPolySupport.normalizedCubeMeasure_originCube_zero_eq_volumeMeasureOn_openCubeSet (d : ℕ) : normalizedCubeMeasure (originCube d 0) = volumeMeasureOn (openCubeSet (originCube d 0))

On the origin unit cube the normalized cube measure is literally volume restricted to the analytic open cube.

theorem HCPolySupport.cubeScaleFactor_originCube_zero (d : ℕ) : cubeScaleFactor (originCube d 0) = 1

The scale factor of the origin unit cube is one.

@[simp]

theorem HCPolySupport.CubeVectorH1Function.relativeGradientCoordL2NormSum_originCube_zero {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) : G.relativeGradientCoordL2NormSum = G.gradientCoordL2NormSum

The internal relative gradient size has no additional geometric factor on the origin unit cube.

theorem HCPolySupport.cubeResidualNorm_le_continuousKResidualNorm {d : ℕ} (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : (cubeLpNorm (originCube d 0) 2 fun (x : Vec d) => F.toField x - G.toCubeVectorH1Function.toField x) ≤ continuousKResidualNorm F G

On the unit cube, the internal ambient-norm residual is bounded by the source Euclidean residual.

theorem HCPolySupport.continuousKResidualNorm_le_dimPlusOne_mul_cubeResidualNorm {d : ℕ} (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : continuousKResidualNorm F G ≤ (↑d + 1) * cubeLpNorm (originCube d 0) 2 fun (x : Vec d) => F.toField x - G.toCubeVectorH1Function.toField x

On the unit cube, the source Euclidean residual is bounded by a positive all-dimension multiple of the internal ambient-norm residual.

theorem HCPolySupport.CubeVectorH1Function.gradientCoordL2NormSum_eq_sum_normalizedELpNorm {d : ℕ} (G : CubeVectorH1Function (originCube d 0)) : G.gradientCoordL2NormSum = ∑ i : Fin d, ∑ j : Fin d, (MeasureTheory.eLpNorm (fun (x : Vec d) => (G.coord i).grad x j) 2 (normalizedCubeMeasure (originCube d 0))).toReal

The internal coordinate-summed gradient norm is the corresponding finite sum of normalized unit-cube L² coordinate norms.

theorem HCPolySupport.continuousKGradientNorm_le_cubeRelativeGradientCoordL2NormSum {d : ℕ} (G : ContinuousKCompetitor d) : continuousKGradientNorm G ≤ G.toCubeVectorH1Function.relativeGradientCoordL2NormSum

The Frobenius L² gradient quantity of a continuous competitor is bounded by the relative coordinate-summed internal gradient quantity on the unit cube.

theorem HCPolySupport.cubeRelativeGradientCoordL2NormSum_le_dimPlusOne_sq_mul_continuousKGradientNorm {d : ℕ} (G : ContinuousKCompetitor d) : G.toCubeVectorH1Function.relativeGradientCoordL2NormSum ≤ (↑d + 1) ^ 2 * continuousKGradientNorm G

The relative coordinate-summed internal gradient quantity is bounded by a positive all-dimension multiple of the source Frobenius L² quantity.

noncomputable def HCPolySupport.continuousDiscreteKBridgeConstant (d : ℕ) : ℝ

One positive, all-dimension constant used uniformly in both directions of the continuous/discrete unit-cube comparison.

Equations

• HCPolySupport.continuousDiscreteKBridgeConstant d = (↑d + 1) ^ 2

theorem HCPolySupport.one_le_continuousDiscreteKBridgeConstant (d : ℕ) : 1 ≤ continuousDiscreteKBridgeConstant d

theorem HCPolySupport.continuousDiscreteKBridgeConstant_nonneg (d : ℕ) : 0 ≤ continuousDiscreteKBridgeConstant d

theorem HCPolySupport.cubeKFunctionalCompetitorValue_le_continuousKFunctionalCompetitorValue_mul {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : cubeVectorKFunctionalCompetitorValue (originCube d 0) (↑t) F.toField G.toCubeVectorH1Function ≤ continuousDiscreteKBridgeConstant d * continuousKFunctionalCompetitorValue t F G

Sending a continuous competitor to the internal cube competitor changes its exact K-functional value by at most the bridge constant.

theorem HCPolySupport.continuousKFunctionalCompetitorValue_le_cubeKFunctionalCompetitorValue_mul {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) (G : CubeVectorH1Function (originCube d 0)) : continuousKFunctionalCompetitorValue t F G.toContinuousKCompetitor ≤ continuousDiscreteKBridgeConstant d * cubeVectorKFunctionalCompetitorValue (originCube d 0) (↑t) F.toField G

Sending an internal cube competitor to the continuous source competitor changes its exact K-functional value by at most the bridge constant.

theorem HCPolySupport.cubeVectorKFunctional_le_mul_continuousKFunctional {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : cubeVectorKFunctional (originCube d 0) (↑t) F.toField ≤ continuousDiscreteKBridgeConstant d * continuousKFunctional t F

The internal discrete K-functional is bounded by the exact continuous K-functional at every source scale, with a d=0-safe constant.

theorem HCPolySupport.continuousKFunctional_le_mul_cubeVectorKFunctional {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : continuousKFunctional t F ≤ continuousDiscreteKBridgeConstant d * cubeVectorKFunctional (originCube d 0) (↑t) F.toField

The exact continuous K-functional is bounded by the internal discrete K-functional at every source scale, with the same d=0-safe constant.