High-contrast homogenization: Analytic.DualNormJunk

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

The dual norms where the printed pairing diverges

The dual norms negSobolevNorm and negOneNorm of e.physical.negative.norm are suprema of per-test normalized pairings. A pairing that is not absolutely convergent has no printed value; a totalized Bochner integral returns 0 for it, and a supremum built on that convention can fall below the printed supremum, so an estimate bounding it can be satisfied by the divergence itself. dualPairing returns ⊤ off the integrable branch instead, and the first two sections record what that does: a single admissible test with a divergent pairing sends the whole dual norm to ⊤, so such an estimate is false rather than satisfiable.

The third section checks that the index family of each supremum is nonempty — the zero test field is admissible — so neither norm is 0 through an empty supremum. The fourth gives the characterization a consumer needs: each dual norm dominates the absolute value of the normalized pairing against every admissible test, the absolute value costing nothing because the admissible family is closed under negation. The last section checks that on the absolutely convergent branch the values are exactly the printed ones.

The convention the ⊤ branch replaces

negSobolevNorm and negOneNorm are suprema of per-test pairings. Under a totalized Bochner integral a pairing that is not absolutely convergent contributes the value 0 to the supremum, so a field with a divergent pairing against an admissible test is assigned a dual norm no larger than the supremum over the remaining tests: the norm is underestimated and the estimates that bound it are satisfied by that failure. The first lemma is that mechanism; the rest is what dualPairing does instead.

theorem HCPolySupport.HighContrast.volumeAverage_eq_zero_of_not_integrableOn {d : ℕ} (V : Set (Vec d)) {f : Vec d → ℝ} (h : ¬MeasureTheory.IntegrableOn f V MeasureTheory.volume) : volumeAverage V f = 0

The mechanism: on a pairing that is not absolutely convergent, the totalized real average vanishes.

theorem HCPolySupport.HighContrast.ofReal_volumeAverage_vecDot_eq_zero_of_not_integrableOn {d : ℕ} (V : Set (Vec d)) (F ψ : Vec d → Vec d) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (ψ x)) V MeasureTheory.volume) : ENNReal.ofReal (volumeAverage V fun (x : Vec d) => vecDot (F x) (ψ x)) = 0

The mechanism, in the form in which it entered the dual norm: the discarded per-test contribution of the previous encoding.

The pairing

theorem HCPolySupport.HighContrast.dualPairing_eq_top_of_not_integrableOn {d : ℕ} (V : Set (Vec d)) (F ψ : Vec d → Vec d) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (ψ x)) V MeasureTheory.volume) : dualPairing V F ψ = ⊤

A divergent pairing is ∞.

theorem HCPolySupport.HighContrast.dualPairing_eq_ofReal {d : ℕ} (V : Set (Vec d)) (F ψ : Vec d → Vec d) (h : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (ψ x)) V MeasureTheory.volume) : dualPairing V F ψ = ENNReal.ofReal (volumeAverage V fun (x : Vec d) => vecDot (F x) (ψ x))

On an absolutely convergent pairing the value is the printed normalized pairing: no value that the reference text writes is changed.

theorem HCPolySupport.HighContrast.negSobolevNorm_eq_top_of_not_integrableOn {d : ℕ} (V : Set (Vec d)) (s : ℝ) (F ψ : Vec d → Vec d) (hψ : IsLocalVecTest V ψ) (hnorm : hsNormSq V s ψ ≤ 1) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (ψ x)) V MeasureTheory.volume) : negSobolevNorm V s F = ⊤

Fail-closed: a single admissible test with a divergent pairing sends the whole dual norm to ∞, so an estimate bounding it by a finite quantity is false rather than satisfiable.

theorem HCPolySupport.HighContrast.negOneNorm_eq_top_of_not_integrableOn {d : ℕ} (V : Set (Vec d)) (F ψ : Vec d → Vec d) (hψ : IsLocalVecTest V ψ) (hnorm : h1NormSq V ψ ≤ 1) (h : ¬MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (ψ x)) V MeasureTheory.volume) : negOneNorm V F = ⊤

The same for the H_underlined^{-1} dual norm.

The index family is nonempty (no empty-supremum junk)

theorem HCPolySupport.HighContrast.vecNormSq_zero_vec {d : ℕ} : vecNormSq 0 = 0

theorem HCPolySupport.HighContrast.isLocalVecTest_zero {d : ℕ} (V : Set (Vec d)) : IsLocalVecTest V fun (x : Vec d) => 0

The zero test field is admissible.

theorem HCPolySupport.HighContrast.isLocalTest_zero {d : ℕ} (V : Set (Vec d)) : IsLocalTest V fun (x : Vec d) => 0

theorem HCPolySupport.HighContrast.eVolumeAverage_zero {d : ℕ} (V : Set (Vec d)) : (eVolumeAverage V fun (x : Vec d) => 0) = 0

theorem HCPolySupport.HighContrast.fracSeminormSq_zero {d : ℕ} (V : Set (Vec d)) (s : ℝ) : (fracSeminormSq V s fun (x : Vec d) => 0) = 0

theorem HCPolySupport.HighContrast.hsNormSq_zero {d : ℕ} (V : Set (Vec d)) (s : ℝ) : (hsNormSq V s fun (x : Vec d) => 0) = 0

theorem HCPolySupport.HighContrast.smoothGrad_zero {d : ℕ} (x : Vec d) : smoothGrad (fun (x : Vec d) => 0) x = 0

theorem HCPolySupport.HighContrast.h1NormSq_zero {d : ℕ} (V : Set (Vec d)) : (h1NormSq V fun (x : Vec d) => 0) = 0

theorem HCPolySupport.HighContrast.negSobolevNorm_zero {d : ℕ} (V : Set (Vec d)) (s : ℝ) : (negSobolevNorm V s fun (x : Vec d) => 0) = 0

The dual norm of the zero field is zero: the supremum is over a nonempty family and the estimates are not junk-true through an empty index.

theorem HCPolySupport.HighContrast.negOneNorm_zero {d : ℕ} (V : Set (Vec d)) : (negOneNorm V fun (x : Vec d) => 0) = 0

The dual norms dominate every admissible pairing

This is the characterization a consumer needs: bounding the dual norm bounds the absolute value of the normalized pairing against every admissible test. The absolute value costs nothing because the admissible family is closed under negation, so the supremum of the signed pairings is already the supremum of their absolute values.

theorem HCPolySupport.HighContrast.isLocalVecTest_neg {d : ℕ} {V : Set (Vec d)} {ψ : Vec d → Vec d} (h : IsLocalVecTest V ψ) : IsLocalVecTest V (-ψ)

theorem HCPolySupport.HighContrast.hsNormSq_neg {d : ℕ} (V : Set (Vec d)) (s : ℝ) (ψ : Vec d → Vec d) : hsNormSq V s (-ψ) = hsNormSq V s ψ

theorem HCPolySupport.HighContrast.ofReal_abs_pairing_le_negSobolevNorm {d : ℕ} (V : Set (Vec d)) (s : ℝ) (F ψ : Vec d → Vec d) (hψ : IsLocalVecTest V ψ) (hnorm : hsNormSq V s ψ ≤ 1) : ENNReal.ofReal |volumeAverage V fun (x : Vec d) => vecDot (F x) (ψ x)| ≤ negSobolevNorm V s F

The H^{-s} dual norm dominates the absolute value of the normalized pairing against every admissible test.

The energies agree with the printed values

Where the quantity the reference text writes is finite, the Lebesgue-integral encoding returns exactly it. No value the reference text writes is changed; the encoding only replaces the totalized 0 by ∞ where the printed quantity is infinite.

theorem HCPolySupport.HighContrast.sEnergyOn_eq_ofReal_integral {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) (F : Vec d → Vec d) (hnonneg : 0 ≤ᵐ[MeasureTheory.volume.restrict V] fun (x : Vec d) => vecDot (F x) (matVecMul (symmPart (b x)) (F x))) (hint : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (F x) (matVecMul (symmPart (b x)) (F x))) V MeasureTheory.volume) : sEnergyOn b V F = ENNReal.ofReal (∫ (x : Vec d) in V, vecDot (F x) (matVecMul (symmPart (b x)) (F x)))

On an absolutely convergent, nonnegative energy the value is the printed one.

theorem HCPolySupport.HighContrast.eVolumeAverage_ofReal_eq {d : ℕ} (V : Set (Vec d)) (f : Vec d → ℝ) (hnonneg : 0 ≤ᵐ[MeasureTheory.volume.restrict V] f) (hint : MeasureTheory.IntegrableOn f V MeasureTheory.volume) : ∫⁻ (x : Vec d) in V, ENNReal.ofReal (f x) = ENNReal.ofReal (∫ (x : Vec d) in V, f x)

The same for the normalized L² average of a square.