High-contrast homogenization: Provider.Regularity.HarmonicAffineDecay #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.CubeCalderonZygmund.exists_harmonic_normalized_affine_candidate_error_decay_at_integer_rate
(d p : ℕ)
[NeZero d]
(hp : 0 < p)
:
∃ (depth : ℕ) (C : ℝ),
0 < C ∧ ∀ (Q : TriadicCube d) (u : H1Function (openCubeSet Q)),
(WeakPoissonEquationOn (openCubeSet Q) u fun (x : Vec d) => 0) →
∀ (c : ℝ) (e : Vec d) (t : ℕ),
have R := centralDescendant (centralDescendant (centralChild (centralChild Q)) depth) (2 * p * t);
∃ (c' : ℝ) (e' : Vec d),
HighContrast.normalizedAffineCandidateError R u.toFun c' e' ≤ C * (1 / 3) ^ ((2 * p - 1) * t) * HighContrast.normalizedAffineCandidateError Q u.toFun c e
theorem
HCPolySupport.CubeCalderonZygmund.exists_identityHarmonic_affineErrorDecay_atIntegerRate
(d p : ℕ)
[NeZero d]
(hp : 0 < p)
:
∃ (depth : ℕ) (C : ℝ),
0 < C ∧ ∀ (t : ℕ),
have N := depth + 2 * p * t + 2;
∀ (k : ℤ) (u : H1Function (openCubeSet (originCube d k))),
(WeakPoissonEquationOn (openCubeSet (originCube d k)) u fun (x : Vec d) => 0) →
∀ (c : ℝ) (e : Vec d),
∃ (c' : ℝ) (e' : Vec d),
HighContrast.normalizedAffineCandidateError (originCube d (k - ↑N)) u.toFun c' e' ≤ C * (1 / 3) ^ ((2 * p - 1) * t) * HighContrast.normalizedAffineCandidateError (originCube d k) u.toFun c e
Identity-cube specialization of the integer-rate affine improvement. At
parameter p, a descent of 2 * p * t variable scales gains the power
(2 * p - 1) * t, up to a fixed initial depth.
theorem
HCPolySupport.CubeCalderonZygmund.exists_identity_harmonic_normalized_affine_candidate_error_decay
(d : ℕ)
[NeZero d]
:
∃ (N : ℕ),
0 < N ∧ ∀ (k : ℤ) (u : H1Function (openCubeSet (originCube d k))),
(WeakPoissonEquationOn (openCubeSet (originCube d k)) u fun (x : Vec d) => 0) →
∀ (c : ℝ) (e : Vec d),
∃ (c' : ℝ) (e' : Vec d),
HighContrast.normalizedAffineCandidateError (originCube d (k - ↑N)) u.toFun c' e' ≤ 1 / 8 * HighContrast.normalizedAffineCandidateError (originCube d k) u.toFun c e
Identity-harmonic functions admit a dimension-only affine improvement on a fixed deeper centered cube.