High-contrast homogenization: Provider.Regularity.UnitCubeContinuousKNormalizedEnergyAddition

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Addition on the normalized unit-cube continuous K-energy

Pointwise addition is packaged on the proof-carrying unit-cube Euclidean L2 carrier. Adding genuine coordinatewise H1 competitors proves the triangle inequality for the continuous K-functional. Squaring that inequality gives the dimension-free factor two for the normalized quadratic energy.

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

The normalized quadratic continuous K-energy used by the unit-cube Dirichlet estimates.

Equations

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

theorem HCPolySupport.HighContrast.unitCubeNormalizedContinuousKEnergy_eq {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : unitCubeNormalizedContinuousKEnergy s F = (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t

Evaluation formula for the normalized quadratic continuous K-energy.

noncomputable def HCPolySupport.HighContrast.unitCubeEuclideanL2FieldAdd {d : ℕ} (F G : UnitCubeEuclideanL2Field d) : UnitCubeEuclideanL2Field d

Pointwise addition, packaged on the unit-cube Euclidean L2 carrier.

Equations

• HCPolySupport.HighContrast.unitCubeEuclideanL2FieldAdd F G = { toField := fun (x : HCPolySupport.Vec d) => F.toField x + G.toField x, euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.unitCubeEuclideanL2FieldAdd_apply {d : ℕ} (F G : UnitCubeEuclideanL2Field d) (x : Vec d) : (unitCubeEuclideanL2FieldAdd F G).toField x = F.toField x + G.toField x

noncomputable def HCPolySupport.HighContrast.continuousKCompetitorAdd {d : ℕ} (G V : ContinuousKCompetitor d) : ContinuousKCompetitor d

Coordinatewise addition of continuous K-functional competitors.

Equations

• HCPolySupport.HighContrast.continuousKCompetitorAdd G V = { coord := fun (i : Fin d) => G.coord i + V.coord i }

theorem HCPolySupport.HighContrast.continuousKFunctional_add_le {d : ℕ} (t : ↑ContinuousKScale) (F H : UnitCubeEuclideanL2Field d) : continuousKFunctional t (unitCubeEuclideanL2FieldAdd F H) ≤ continuousKFunctional t F + continuousKFunctional t H

Pointwise addition obeys the triangle inequality for the continuous K-functional.

theorem HCPolySupport.HighContrast.continuousKSeminormIntegrand_add_le {d : ℕ} (sigma : ℝ) (F H : UnitCubeEuclideanL2Field d) (t : ℝ) : continuousKSeminormIntegrand sigma (unitCubeEuclideanL2FieldAdd F H) t ≤ 2 * continuousKSeminormIntegrand sigma F t + 2 * continuousKSeminormIntegrand sigma H t

The continuous K-seminorm integrand of a pointwise sum is bounded by twice the corresponding integrand of each summand.

theorem HCPolySupport.HighContrast.continuousKSeminormIntegral_add_le {d : ℕ} (sigma : ℝ) (F H : UnitCubeEuclideanL2Field d) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand sigma (unitCubeEuclideanL2FieldAdd F H) t ≤ (2 * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand sigma F t) + 2 * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand sigma H t

The continuous K-seminorm integral of a pointwise sum is bounded by twice the corresponding integral of each summand.

theorem HCPolySupport.HighContrast.unitCubeNormalizedEuclideanLpENorm_add_le {d : ℕ} (F H : UnitCubeEuclideanL2Field d) : (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeEuclideanL2FieldAdd F H).toField ≤ (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField + (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 H.toField

Minkowski's inequality for pointwise addition on the normalized unit-cube Euclidean L2 term.

theorem HCPolySupport.HighContrast.unitCubeNormalizedContinuousKEnergy_add_le {d : ℕ} (s : ↑FractionalOrder) (F H : UnitCubeEuclideanL2Field d) : unitCubeNormalizedContinuousKEnergy s (unitCubeEuclideanL2FieldAdd F H) ≤ 2 * unitCubeNormalizedContinuousKEnergy s F + 2 * unitCubeNormalizedContinuousKEnergy s H

Pointwise addition costs at most a factor two on each input in the normalized quadratic continuous K-energy.