High-contrast homogenization: Provider.Regularity.FiniteLipschitzCoreBase

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

Shared analytic core for finite large-scale regularity

This module contains the common affine approximation, replacement, and Poincare estimates used by the recurrence and best-fit branches.

noncomputable def HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzRestriction {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : Book.Ch03.CubeSolution (originCube d (min k m)) a

Restrict a solution on the origin cube at scale m to scale min k m, so the requested local scale never exceeds its domain.

Equations

• HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzRestriction a m u k = HCPolySupport.HighContrast.finiteCubeSolutionRestriction a ⋯ u

@[simp]

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzRestriction_toFun {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : (finiteLipschitzRestriction a m u k).toH1.toFun = u.toH1.toFun

@[simp]

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzRestriction_grad {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : (finiteLipschitzRestriction a m u k).toH1.grad = u.toH1.grad

noncomputable def HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : ℝ

The coefficient-weighted H¹ energy norm of the solution on the origin cube at scale min k m.

Equations

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

noncomputable def HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzBestIntercept {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : ℝ

The intercept of the L² best affine fit to the restricted solution on the origin cube at scale min k m.

Equations

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

noncomputable def HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzBestSlope {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : Vec d

The slope of the L² best affine fit to the restricted solution on the origin cube at scale min k m.

Equations

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

noncomputable def HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : ℝ

The normalized affine approximation error of the restricted solution, using its best-fit intercept and slope at scale min k m.

Equations

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

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow_nonneg {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : 0 ≤ finiteLipschitzEnergyRow a m u k

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow_eq_h1EnergyNormOnCube_of_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m) : finiteLipschitzEnergyRow a m u k = Book.Ch03.h1EnergyNormOnCube (originCube d k) a (finiteCubeSolutionRestriction a hkm u).toH1

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzEnergyRow_self {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) : finiteLipschitzEnergyRow a m u m = Book.Ch03.h1EnergyNormOnCube (originCube d m) a u.toH1

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow_nonneg {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) : 0 ≤ finiteLipschitzAffineErrorRow a m u k

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.solutionEnergyNorm_eq_h1EnergyNormOnCube {d : ℕ} (Q : TriadicCube d) (a : Book.Ch03.CoeffFamily d) (u : Book.Ch03.CubeSolution Q a) : Book.Ch03.solutionEnergyNorm Q a u = Book.Ch03.h1EnergyNormOnCube Q a u.toH1

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.cubeBesovScaleWeight_one_originCube_sub_nat {d : ℕ} (k : ℤ) (N : ℕ) : cubeBesovScaleWeight 1 (originCube d (k - ↑N)) = 3 ^ N * cubeBesovScaleWeight 1 (originCube d k)

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.cubeLpNorm_originCube_sub_nat_le {d : ℕ} (k : ℤ) (N : ℕ) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure (originCube d k))) : cubeLpNorm (originCube d (k - ↑N)) 2 f ≤ ↑((3 ^ d) ^ N) * cubeLpNorm (originCube d k) 2 f

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.normalizedCubeL2Distance_originCube_sub_nat_le {d : ℕ} (k : ℤ) (N : ℕ) (f g : Vec d → ℝ) (hfg : MeasureTheory.MemLp (fun (x : Vec d) => f x - g x) 2 (normalizedCubeMeasure (originCube d k))) : normalizedCubeL2Distance (originCube d (k - ↑N)) f g ≤ 3 ^ N * ↑((3 ^ d) ^ N) * normalizedCubeL2Distance (originCube d k) f g

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.cubeSolution_isWeakSolutionOn {d : ℕ} {Q : TriadicCube d} {a : Book.Ch03.CoeffFamily d} (u : Book.Ch03.CubeSolution Q a) : IsWeakSolutionOn (a.coeffOn Q).toCoeffField (Book.Ch02.cubeDomain Q).carrier u.toH1.grad

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.identityReplacement_weakPoisson {d : ℕ} (a : Book.Ch03.CoeffFamily d) (k : ℤ) (u : H1Function (Book.Ch02.cubeDomain (originCube d k)).carrier) (hu : IsWeakSolutionOn (a.coeffOn (originCube d k)).toCoeffField (Book.Ch02.cubeDomain (originCube d k)).carrier u.grad) : WeakPoissonEquationOn (openCubeSet (originCube d k)) (identityHarmonicReplacementDatum a k u hu).v fun (x : Vec d) => 0

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.originCubeAffineH1LinearMap_weakPoisson (d : ℕ) (k : ℤ) (p : AffineCoefficients d) : WeakPoissonEquationOn (openCubeSet (originCube d k)) ((originCubeAffineH1LinearMap d k) p) fun (x : Vec d) => 0

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.normalizedAffineCandidateError_originCube_sub_nat_le {d : ℕ} (k : ℤ) (N : ℕ) (f : Vec d → ℝ) (c : ℝ) (e : Vec d) (hmem : MeasureTheory.MemLp (fun (x : Vec d) => f x - (c + vecDot e x)) 2 (normalizedCubeMeasure (originCube d k))) : normalizedAffineCandidateError (originCube d (k - ↑N)) f c e ≤ 3 ^ N * ↑((3 ^ d) ^ N) * normalizedAffineCandidateError (originCube d k) f c e

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.normalizedAffineCandidateError_zero_sub_le_add {d : ℕ} (Q : TriadicCube d) (f : 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) => f x - (c₂ + vecDot e₂ x)) 2 (normalizedCubeMeasure Q)) : normalizedAffineCandidateError Q (fun (x : Vec d) => 0) (c₁ - c₂) (e₁ - e₂) ≤ normalizedAffineCandidateError Q f c₁ e₁ + normalizedAffineCandidateError Q f c₂ e₂

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_originCubeAffineSlopeErrorConstant (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (k : ℤ) (c : ℝ) (e : Vec d), euclideanNorm e ≤ C * normalizedAffineCandidateError (originCube d k) (fun (x : Vec d) => 0) c e

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzBestResidual_memLp {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) {k : ℤ} (hkm : k ≤ m) : MeasureTheory.MemLp (fun (x : Vec d) => u.toH1.toFun x - (finiteLipschitzBestIntercept a m u k + vecDot (finiteLipschitzBestSlope a m u k) x)) 2 (normalizedCubeMeasure (originCube d k))

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteLipschitzAffineErrorRow_best_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) {k : ℤ} (hkm : k ≤ m) (c : ℝ) (e : Vec d) : finiteLipschitzAffineErrorRow a m u k ≤ normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzAdjacentSlopeConstant (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ), k + 1 ≤ m → euclideanNorm (finiteLipschitzBestSlope a m u k - finiteLipschitzBestSlope a m u (k + 1)) ≤ C * (finiteLipschitzAffineErrorRow a m u k + finiteLipschitzAffineErrorRow a m u (k + 1))

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.poincareLowerEllipticityFactor_finite_two_eq_sqrt_inv {d : ℕ} (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) {s : ℝ} : Book.Ch03.poincareLowerEllipticityFactor Q a s (Book.Ch02.MultiscaleExponent.finite 2) = √(Book.Ch02.lambdaSq Q s (Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.scalarIdentityWeakError_le_one_lowerEllipticity {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {s : ℝ} (hs : 0 < s) {k : ℤ} (herror : scalarIdentityWeakError a s k ≤ 1) : (Book.Ch02.lambdaSq (originCube d k) s (Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ 4 * ↑d

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.scalarIdentityWeakError_le_one_qoneEllipticity {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {s r : ℝ} (hs : 0 < s) (hsr : s < r) {k : ℤ} (herror : scalarIdentityWeakError a s k ≤ 1) : Book.Ch02.LambdaS (originCube d k) r a ≤ exponentGapFactor s r * (4 * ↑d) ∧ (Book.Ch02.lambdaS (originCube d k) r a)⁻¹ ≤ exponentGapFactor s r * (4 * ↑d)

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.caccioppoliPrefactor_weakError_le_one {d : ℕ} [NeZero d] {C₀ s r : ℝ} (hC₀ : 0 < C₀) (hs : 0 < s) (hsr : s < r) (hr_lt : r < 1 / 2) {a : Book.Ch02.TriadicCoeffFamily d} {k : ℤ} (herror : scalarIdentityWeakError a s k ≤ 1) : have D := exponentGapFactor s r * (4 * ↑d); have α := r / (1 - 2 * r); have K := (C₀ / (1 - 2 * r)).rpow (2 + 4 * r / (1 - 2 * r)) * r.rpow (-(2 * r / (1 - 2 * r))) * (D * D).rpow α * D; Book.Ch03.caccioppoliPrefactor C₀ (originCube d k) a r r ≤ K * cubeBesovScaleWeight 1 (originCube d k) ^ 2

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.finiteCubeRestriction_sub_two_energy_eq_coreEnergy {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a) : Book.Ch03.h1EnergyNormOnCube (originCube d (k - 2)) a (finiteCubeSolutionRestriction a ⋯ u).toH1 = √(Book.Ch03.interiorCaccioppoliCoreEnergy (originCube d k) a (cubeCenter (originCube d k)) u)

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzCaccioppoliAffineConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a) (c : ℝ) (e : Vec d), scalarIdentityWeakError a s k ≤ 1 → Book.Ch03.h1EnergyNormOnCube (originCube d (k - 2)) a (finiteCubeSolutionRestriction a ⋯ u).toH1 ≤ C * (normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e + euclideanNorm e)

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.normalizedCubeL2Distance_comm {d : ℕ} (Q : TriadicCube d) (f g : Vec d → ℝ) : normalizedCubeL2Distance Q f g = normalizedCubeL2Distance Q g f

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzOneStepConstant_of_harmonic_decay (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (N : ℕ) (hN : 0 < N) (theta : ℝ) (htheta : 0 < theta) (hdecay : ∀ (k : ℤ) (v : H1Function (openCubeSet (originCube d k))), (WeakPoissonEquationOn (openCubeSet (originCube d k)) v fun (x : Vec d) => 0) → ∀ (c : ℝ) (e : Vec d), ∃ (c' : ℝ) (e' : Vec d), normalizedAffineCandidateError (originCube d (k - ↑N)) v.toFun c' e' ≤ theta * normalizedAffineCandidateError (originCube d k) v.toFun c e) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a), ∀ k ≤ m, finiteLipschitzAffineErrorRow a m u (k - ↑N) ≤ theta * finiteLipschitzAffineErrorRow a m u k + C * scalarIdentityWeakError a s k * finiteLipschitzEnergyRow a m u k

theorem HCPolySupport.HighContrast.FiniteLipschitzCoreInternal.exists_finiteLipschitzOneStepConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (N : ℕ), 0 < N ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a), ∀ k ≤ m, finiteLipschitzAffineErrorRow a m u (k - ↑N) ≤ 1 / 8 * finiteLipschitzAffineErrorRow a m u k + C * scalarIdentityWeakError a s k * finiteLipschitzEnergyRow a m u k

theorem HCPolySupport.HighContrast.exists_finiteLipschitzPoincareConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a), scalarIdentityWeakError a s k ≤ 1 → cubeBesovScaleWeight 1 (originCube d k) * cubeLpNorm (originCube d k) 2 (cubeFluctuation (originCube d k) u.toH1.toFun) ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) a u.toH1