Coarse-graining support: Support.Deterministic.CoarseCaccioppoliLocalGradientBridge #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.abs_cubeAverage_vecDot_grad_le_note_terms_of_partialBounds_of_h10OnCube
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(u : Vec d → Vec d)
(φ : H10Function (cubeSet Q))
{Bu Bg : ℝ}
(hs : 0 < s)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hgrad : MeasureTheory.MemLp (fun (x : Vec d) => φ.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => φ.grad x) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (u x) (φ.grad x)| ≤ ∑ i : Fin d,
(3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeAverage_energy_identity_sub_const
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))]
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(hmem : MemVectorL2 (cubeSet Q) g)
(c : Vec d)
:
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.cubeAverage_coefficientEnergy_identity_sub_const
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
[MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))]
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(hmem : MemVectorL2 (cubeSet Q) g)
(c : Vec d)
:
cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) = cubeAverage Q fun (x : Vec d) => vecDot (g x - c) (ρ.toH10.grad x)
Corrector identity averaged in the intrinsic coefficient energy.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_note_terms_of_partialBounds_sub_const
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s : ℝ)
(c : Vec d)
{Bu Bg : ℝ}
(hs : 0 < s)
(hmem : MemVectorL2 (cubeSet Q) g)
(hu : MeasureTheory.MemLp (fun (x : Vec d) => g x - c) 2 (normalizedCubeMeasure Q))
(hgrad : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminorm Q s N fun (x : Vec d) => g x - c) ≤ Bu)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => ρ.toH10.grad x) ≤ Bg)
:
cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ ∑ i : Fin d,
(3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => (g x - c) i‖) * (cubeBesovScaleWeight s Q * Bg)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.abs_cubeAverage_vecDot_grad_le_note_terms_of_partialBounds_of_h10OnCube_two_two
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
(u : Vec d → Vec d)
(φ : H10Function (cubeSet Q))
{Bu Bg : ℝ}
(hs : 0 < s)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(hgrad : MeasureTheory.MemLp (fun (x : Vec d) => φ.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => φ.grad x) ≤ Bg)
:
|cubeAverage Q fun (x : Vec d) => vecDot (u x) (φ.grad x)| ≤ ∑ i : Fin d,
(3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_note_terms_of_partialBounds_sub_const_two_two
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s : ℝ)
(c : Vec d)
{Bu Bg : ℝ}
(hs : 0 < s)
(hmem : MemVectorL2 (cubeSet Q) g)
(hu : MeasureTheory.MemLp (fun (x : Vec d) => g x - c) 2 (normalizedCubeMeasure Q))
(hgrad : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - c) ≤ Bu)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => ρ.toH10.grad x) ≤ Bg)
:
cubeAverage Q (coefficientEnergyDensity a fun (x : Vec d) => ρ.toH10.grad x) ≤ ∑ i : Fin d,
(3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => (g x - c) i‖) * (cubeBesovScaleWeight s Q * Bg)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.coefficientEnergy_average_le_collapsed_note_term_centered_two_two
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
(s : ℝ)
{Bρ Bg : ℝ}
(hs : 0 < s)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgrad : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ Bg)
(hneg : ∀ (N : ℕ), (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => ρ.toH10.grad x) ≤ Bρ)
(hpos : ∀ (N : ℕ), (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g) ≤ Bg)
: