Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.LocalCorrector #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeAverageVec_eq_of_eq_add_grad_on_cubeSet
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u v : Vec d → Vec d}
(huv : ∀ x ∈ cubeSet Q, u x = v x + ρ.toH10.grad x)
(hv : MemVectorL2 (cubeSet Q) v)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_two_mul_add
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hu : MemVectorL2 (cubeSet Q) u)
(s : ℝ)
(N : ℕ)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_sqrtTwo_mul_add
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hu : MemVectorL2 (cubeSet Q) u)
(s : ℝ)
(N : ℕ)
:
(cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ρ.toH10.grad x) ≤ √2 * (cubeBesovNegativeVectorPartialSeminormTwo Q s N u + cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_sqrtTwo_mul_add_of_bounds
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hu : MemVectorL2 (cubeSet Q) u)
(s : ℝ)
{Bu Bw : ℝ}
(huB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu)
(hwB : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) ≤ Bw)
(N : ℕ)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeBesovNegativeVectorPartialSeminormTwo_corrector_le_sqrtTwo_mul_add_of_bddAbove
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hu : MemVectorL2 (cubeSet Q) u)
(s : ℝ)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(N : ℕ)
:
(cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ρ.toH10.grad x) ≤ √2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x)