Coarse-graining support: Support.Sobolev.Fractional.ContinuousKFunctional

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

The continuous centered-cube K-functional

This is the literal real-interpolation kernel from the Chapter 1 constant-coefficient Dirichlet argument. The unit centered open cube is used for the coordinatewise H¹ competitors; normalized volume is realized by its a.e.-equal half-open cube.

@[reducible, inline]

abbrev HCPolySupport.ContinuousKScale : Set ℝ

The source scale carrier 0 < t ≤ 1.

Equations

• HCPolySupport.ContinuousKScale = Set.Ioc 0 1

theorem HCPolySupport.ContinuousKScale.pos (t : ↑ContinuousKScale) : 0 < ↑t

theorem HCPolySupport.ContinuousKScale.le_one (t : ↑ContinuousKScale) : ↑t ≤ 1

structure HCPolySupport.ContinuousKCompetitor (d : ℕ) : Type

A source-faithful H¹(square_0; ℝ^d) competitor. Its coordinates carry genuine H1Function witnesses on the source-facing open cube.

• coord : Fin d → H1Function (openCubeSet (originCube d 0))

  One genuine weak H¹ witness for each target coordinate.

def HCPolySupport.ContinuousKCompetitor.toField {d : ℕ} (G : ContinuousKCompetitor d) : Vec d → Vec d

The vector field represented by a coordinatewise H¹ competitor.

Equations

• G.toField x i = (G.coord i).toFun x

def HCPolySupport.ContinuousKCompetitor.gradient {d : ℕ} (G : ContinuousKCompetitor d) : Vec d → Mat d

The matrix of actual coordinate weak gradients.

Equations

• G.gradient x i j = (G.coord i).grad x j

@[simp]

theorem HCPolySupport.ContinuousKCompetitor.toField_apply {d : ℕ} (G : ContinuousKCompetitor d) (x : Vec d) (i : Fin d) : G.toField x i = (G.coord i).toFun x

@[simp]

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

@[instance_reducible]

instance HCPolySupport.ContinuousKCompetitor.instInhabited {d : ℕ} : Inhabited (ContinuousKCompetitor d)

Equations

• HCPolySupport.ContinuousKCompetitor.instInhabited = { default := { coord := fun (x : Fin d) => 0 } }

theorem HCPolySupport.ContinuousKCompetitor.euclideanMemL2 {d : ℕ} (G : ContinuousKCompetitor d) : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (G.toField x)) 2 (unitCenteredCubeDomain d).normalizedVolume

Euclidean L² control of the represented field, derived solely from the coordinate H¹ witnesses.

theorem HCPolySupport.ContinuousKCompetitor.gradientFrobeniusMemL2 {d : ℕ} (G : ContinuousKCompetitor d) : MeasureTheory.MemLp (fun (x : Vec d) => matrixFrobeniusMagnitude (G.gradient x)) 2 (unitCenteredCubeDomain d).normalizedVolume

Frobenius L² control of the actual weak-gradient matrix, derived from the coordinate H¹ witnesses and the shared Frobenius realization.

noncomputable def HCPolySupport.continuousKResidualNorm {d : ℕ} (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : ℝ

The normalized Euclidean L² residual in the continuous K-functional.

Equations

• HCPolySupport.continuousKResidualNorm F G = (HCPolySupport.unitCenteredCubeDomain d).normalizedEuclideanLpNorm 2 (fun (x : HCPolySupport.Vec d) => F.toField x - G.toField x) ⋯

noncomputable def HCPolySupport.continuousKGradientNorm {d : ℕ} (G : ContinuousKCompetitor d) : ℝ

The normalized Frobenius L² weak-gradient quantity in the continuous K-functional.

Equations

• HCPolySupport.continuousKGradientNorm G = (HCPolySupport.unitCenteredCubeDomain d).normalizedLpNorm 2 (fun (x : HCPolySupport.Vec d) => HCPolySupport.matrixFrobeniusMagnitude (G.gradient x)) ⋯

theorem HCPolySupport.continuousKResidualNorm_nonneg {d : ℕ} (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : 0 ≤ continuousKResidualNorm F G

theorem HCPolySupport.continuousKGradientNorm_nonneg {d : ℕ} (G : ContinuousKCompetitor d) : 0 ≤ continuousKGradientNorm G

noncomputable def HCPolySupport.continuousKFunctionalCompetitorValue {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : ℝ

The exact square-root value contributed by one genuine H¹ competitor.

Equations

• HCPolySupport.continuousKFunctionalCompetitorValue t F G = √(HCPolySupport.continuousKResidualNorm F G ^ 2 + ↑t ^ 2 * HCPolySupport.continuousKGradientNorm G ^ 2)

theorem HCPolySupport.continuousKFunctionalCompetitorValue_nonneg {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : 0 ≤ continuousKFunctionalCompetitorValue t F G

theorem HCPolySupport.continuousKFunctionalCompetitorValue_mono {d : ℕ} {t u : ↑ContinuousKScale} (htu : ↑t ≤ ↑u) (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : continuousKFunctionalCompetitorValue t F G ≤ continuousKFunctionalCompetitorValue u F G

noncomputable def HCPolySupport.continuousKFunctional {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : ℝ

The literal continuous real-interpolation K-functional.

Equations

• HCPolySupport.continuousKFunctional t F = sInf (Set.range fun (G : HCPolySupport.ContinuousKCompetitor d) => HCPolySupport.continuousKFunctionalCompetitorValue t F G)

theorem HCPolySupport.continuousKFunctional_eq_sInf {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : continuousKFunctional t F = sInf (Set.range fun (G : ContinuousKCompetitor d) => continuousKFunctionalCompetitorValue t F G)

theorem HCPolySupport.continuousKFunctional_range_nonempty {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : (Set.range fun (G : ContinuousKCompetitor d) => continuousKFunctionalCompetitorValue t F G).Nonempty

theorem HCPolySupport.continuousKFunctional_range_bddBelow {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : BddBelow (Set.range fun (G : ContinuousKCompetitor d) => continuousKFunctionalCompetitorValue t F G)

theorem HCPolySupport.continuousKFunctional_nonneg {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) : 0 ≤ continuousKFunctional t F

theorem HCPolySupport.continuousKFunctional_le_competitor {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) (G : ContinuousKCompetitor d) : continuousKFunctional t F ≤ continuousKFunctionalCompetitorValue t F G

theorem HCPolySupport.continuousKFunctional_mono {d : ℕ} {t u : ↑ContinuousKScale} (htu : ↑t ≤ ↑u) (F : UnitCubeEuclideanL2Field d) : continuousKFunctional t F ≤ continuousKFunctional u F

noncomputable def HCPolySupport.continuousKFunctionalOnOpenScale {d : ℕ} (F : UnitCubeEuclideanL2Field d) (t : ℝ) : ℝ

The real-line representative of K(t,F) used for the continuum integral. It agrees with the source K-functional on the open integration interval.

Equations

• HCPolySupport.continuousKFunctionalOnOpenScale F t = if ht : t ∈ Set.Ioo 0 1 then HCPolySupport.continuousKFunctional ⟨t, ⋯⟩ F else 0

theorem HCPolySupport.continuousKFunctionalOnOpenScale_monoOn {d : ℕ} (F : UnitCubeEuclideanL2Field d) : MonotoneOn (continuousKFunctionalOnOpenScale F) (Set.Ioo 0 1)

theorem HCPolySupport.continuousKFunctionalOnOpenScale_aemeasurable {d : ℕ} (F : UnitCubeEuclideanL2Field d) : AEMeasurable (continuousKFunctionalOnOpenScale F) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

noncomputable def HCPolySupport.continuousKSeminormIntegrand {d : ℕ} (s : ℝ) (F : UnitCubeEuclideanL2Field d) (t : ℝ) : ENNReal

The nonnegative integrand in the continuum K-seminorm. On the exact integration interval it is t^(-2s) K(t,F)^2 / t.

Equations

• HCPolySupport.continuousKSeminormIntegrand s F t = ENNReal.ofReal (t.rpow (-2 * s)) * ENNReal.ofReal (HCPolySupport.continuousKFunctionalOnOpenScale F t ^ 2) * ENNReal.ofReal t⁻¹

theorem HCPolySupport.continuousKSeminormIntegrand_aemeasurable {d : ℕ} (s : ℝ) (F : UnitCubeEuclideanL2Field d) : AEMeasurable (continuousKSeminormIntegrand s F) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem HCPolySupport.continuousKSeminormIntegrand_eq_of_mem {d : ℕ} (s : ℝ) (F : UnitCubeEuclideanL2Field d) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : continuousKSeminormIntegrand s F t = ENNReal.ofReal (t.rpow (-2 * s)) * ENNReal.ofReal (continuousKFunctional ⟨t, ⋯⟩ F ^ 2) * ENNReal.ofReal t⁻¹

On the source integration interval, the integrand is literally the weighted square t^(-2s) K(t,F)^2 / t.

noncomputable def HCPolySupport.continuousKSeminorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : ENNReal

The exact ENNReal-valued continuum interpolation seminorm. Its integrand is a genuine Lebesgue-measurable function on (0,1), rather than a lower- integral convention for an unverified representative.

Equations

• HCPolySupport.continuousKSeminorm s F = (∫⁻ (t : ℝ) in Set.Ioo 0 1, HCPolySupport.continuousKSeminormIntegrand (↑s) F t) ^ (1 / 2)

theorem HCPolySupport.continuousKSeminorm_eq_lintegral {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : continuousKSeminorm s F = (∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t) ^ (1 / 2)

Exact continuum-lintegral characterization of the interpolation seminorm, including the source weight t^(-2s) and measure factor dt / t.

theorem HCPolySupport.continuousKResidualNorm_congr_ae {d : ℕ} {F H : UnitCubeEuclideanL2Field d} (G : ContinuousKCompetitor d) (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) : continuousKResidualNorm F G = continuousKResidualNorm H G

theorem HCPolySupport.continuousKFunctionalCompetitorValue_congr_ae {d : ℕ} (t : ↑ContinuousKScale) {F H : UnitCubeEuclideanL2Field d} (G : ContinuousKCompetitor d) (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) : continuousKFunctionalCompetitorValue t F G = continuousKFunctionalCompetitorValue t H G

theorem HCPolySupport.continuousKFunctional_congr_ae {d : ℕ} (t : ↑ContinuousKScale) {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) : continuousKFunctional t F = continuousKFunctional t H

theorem HCPolySupport.continuousKFunctionalOnOpenScale_congr_ae {d : ℕ} {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) (t : ℝ) : continuousKFunctionalOnOpenScale F t = continuousKFunctionalOnOpenScale H t

theorem HCPolySupport.continuousKSeminormIntegrand_congr_ae {d : ℕ} (s : ℝ) {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) (t : ℝ) : continuousKSeminormIntegrand s F t = continuousKSeminormIntegrand s H t

theorem HCPolySupport.continuousKSeminorm_congr_ae {d : ℕ} (s : ↑FractionalOrder) {F H : UnitCubeEuclideanL2Field d} (hFH : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] H.toField) : continuousKSeminorm s F = continuousKSeminorm s H