High-contrast homogenization: Provider.Regularity.FiniteAffineGradientResidual

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

Finite affine gradient residuals

This module realizes the difference between a finite cube solution and a finite affine-boundary solution as an actual harmonic solution on every smaller centered cube. It is the bridge from the gradient-excess definition to the finite Caccioppoli estimates.

theorem HCPolySupport.HighContrast.weightedGradNorm_congr_ae {d : ℕ} (b : CoeffField d) (V : Set (Vec d)) {F G : Vec d → Vec d} (hFG : F =ᵐ[volumeMeasureOn V] G) : weightedGradNorm b V F = weightedGradNorm b V G

The weighted gradient norm respects almost-everywhere equality on its integration set.

theorem HCPolySupport.HighContrast.normalizedAffineCandidateError_sub_le_add {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) (c₁ c₂ : ℝ) (e₁ e₂ : Vec d) (h₁ : MeasureTheory.MemLp (fun (x : Vec d) => f x - (c₁ + vecDot e₁ x)) 2 (normalizedCubeMeasure Q)) (h₂ : MeasureTheory.MemLp (fun (x : Vec d) => g x - (c₂ + vecDot e₂ x)) 2 (normalizedCubeMeasure Q)) : normalizedAffineCandidateError Q (fun (x : Vec d) => f x - g x) (c₁ - c₂) (e₁ - e₂) ≤ normalizedAffineCandidateError Q f c₁ e₁ + normalizedAffineCandidateError Q g c₂ e₂

Subtracting two fields and their affine candidates costs at most the sum of the two candidate errors.

theorem HCPolySupport.HighContrast.cubeSolution_weakFluxIntegrable_finiteAffineGradientResidual {d : ℕ} {Q : TriadicCube d} {a : Book.Ch02.TriadicCoeffFamily d} (u : Book.Ch03.CubeSolution Q a) : weakFluxIntegrable (Book.Ch02.cubeDomain Q).carrier (a.coeffOn Q).toCoeffField u

noncomputable def HCPolySupport.HighContrast.finiteAffineGradientResidual {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : Book.Ch03.CubeSolution (originCube d n) a

The harmonic residual u - w_m(e) on the centered cube Q_n.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineGradientResidual_toFun {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : (finiteAffineGradientResidual a hnm u e).toH1.toFun = fun (x : Vec d) => u.toH1.toFun x - (finiteAffineSolution a m e).toH1.toFun x

The residual has the literal value representative u - w_m(e).

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineGradientResidual_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : (finiteAffineGradientResidual a hnm u e).toH1.grad = fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m e).toH1.grad x

The residual has the literal gradient representative ∇u - ∇w_m(e).

theorem HCPolySupport.HighContrast.weightedGradNorm_finiteAffineGradientResidual {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : (weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m e).toH1.grad x) = ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube (originCube d n) a (finiteAffineGradientResidual a hnm u e).toH1)

A gradient-excess candidate is exactly the ENNReal realization of the cube energy of its harmonic residual.

theorem HCPolySupport.HighContrast.finiteAffineGradientExcess_le_residualEnergy {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e : Vec d) : finiteAffineGradientExcess a n m u ≤ ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube (originCube d n) a (finiteAffineGradientResidual a hnm u e).toH1)

The canonical excess is bounded by the energy of every harmonic affine residual.

noncomputable def HCPolySupport.HighContrast.finiteAffineGradientUpdatedResidual {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {k m : ℤ} (hkm : k ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e p : Vec d) : Book.Ch03.CubeSolution (originCube d k) a

The residual u - w_m(e) - w_m(p) realized as a harmonic solution on Q_k. Both affine solutions retain the original outer scale m.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineGradientUpdatedResidual_toFun {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {k m : ℤ} (hkm : k ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e p : Vec d) : (finiteAffineGradientUpdatedResidual a hkm u e p).toH1.toFun = fun (x : Vec d) => u.toH1.toFun x - (finiteAffineSolution a m e).toH1.toFun x - (finiteAffineSolution a m p).toH1.toFun x

The updated residual has the literal value representative u - w_m(e) - w_m(p).

@[simp]

theorem HCPolySupport.HighContrast.finiteAffineGradientUpdatedResidual_grad {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {k m : ℤ} (hkm : k ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e p : Vec d) : (finiteAffineGradientUpdatedResidual a hkm u e p).toH1.grad = fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m e).toH1.grad x - (finiteAffineSolution a m p).toH1.grad x

The updated residual has gradient ∇u - ∇w_m(e) - ∇w_m(p).

theorem HCPolySupport.HighContrast.weightedGradNorm_finiteAffineGradientUpdatedResidual {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {j k m : ℤ} (hjk : j ≤ k) (hkm : k ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e p : Vec d) : weightedGradNorm (a.coeffOn (originCube d j)).toCoeffField (openCubeSet (originCube d j)) (finiteCubeSolutionRestriction a hjk (finiteAffineGradientUpdatedResidual a hkm u e p)).toH1.grad = weightedGradNorm (a.coeffOn (originCube d j)).toCoeffField (openCubeSet (originCube d j)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m (e + p)).toH1.grad x

Updating an outer affine residual is, in weighted gradient norm, the same as updating its outer boundary slope by addition.

theorem HCPolySupport.HighContrast.finiteAffineGradientExcess_le_updatedResidualEnergy {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {j k m : ℤ} (hjk : j ≤ k) (hkm : k ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (e p : Vec d) : finiteAffineGradientExcess a j m u ≤ ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube (originCube d j) a (finiteCubeSolutionRestriction a hjk (finiteAffineGradientUpdatedResidual a hkm u e p)).toH1)

Every updated outer residual gives a candidate upper bound for the original solution's gradient excess.

theorem HCPolySupport.HighContrast.finiteAffineGradientExcess_le_mul_of_forall_candidate {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {j k m : ℤ} (u : Book.Ch03.CubeSolution (originCube d m) a) (q : ENNReal) (hq_zero : q ≠ 0) (hq_top : q ≠ ⊤) (hpointwise : ∀ (e : Vec d), finiteAffineGradientExcess a j m u ≤ q * weightedGradNorm (a.coeffOn (originCube d k)).toCoeffField (openCubeSet (originCube d k)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m e).toH1.grad x) : finiteAffineGradientExcess a j m u ≤ q * finiteAffineGradientExcess a k m u

A pointwise contraction for every affine residual descends to the canonical infimum without assuming that the infimum is attained.