Weighted pointwise bound for ∇ ∇·(B ∇T) #
sc_gradDiv_vecNormSq_le loses the factor r² on every term of the Leibniz expansion.
Here the coefficient of order p is weighted by L^{|p|} and the corresponding word of T of
order
2 - |p| keeps the weight L^{2-|p|}, so that with the T jets at the same rate L the total
loss
is a single factor L² (the source gets ε_{m-1}^{-2-γ} from ∇³ T, ∇² T ∇B, ∇T ∇²B).
noncomputable def
AVenhance.Infra.Section5.Contracts.seWordSum
(L : ℝ)
(v : Homogenization.Vec 2 → ℝ)
(x : Homogenization.Vec 2)
:
The weighted word sum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Section5.Contracts.se_flux_term_abs_le
{A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{v : Homogenization.Vec 2 → ℝ}
(x : Homogenization.Vec 2)
{D L : ℝ}
(hD : 0 ≤ D)
(hL : 0 ≤ L)
(hAj :
∀ (p : List (Fin 2)),
p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord A p x j k| ≤ D * ↑p.length.factorial * L ^ p.length)
(w : List (Fin 2))
(hw : w.length = 2)
{p : List (Fin 2) × List (Fin 2)}
(hp : p ∈ Section4.iterateSpatialSplits w)
(k j : Fin 2)
:
|Section4.iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A y k j) x * spaceGrad (Section4.iterateSpatialWord p.2 v) x j| ≤ 2 * D * seWordSum L v x
theorem
AVenhance.Infra.Section5.Contracts.se_gradDiv_abs_le
{A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{v : Homogenization.Vec 2 → ℝ}
(hA : ContDiff ℝ (↑⊤) A)
(hv : ContDiff ℝ (↑⊤) v)
(x : Homogenization.Vec 2)
{D L : ℝ}
(hD : 0 ≤ D)
(hL : 0 ≤ L)
(hAj :
∀ (p : List (Fin 2)),
p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord A p x j k| ≤ D * ↑p.length.factorial * L ^ p.length)
(i : Fin 2)
:
theorem
AVenhance.Infra.Section5.Contracts.se_gradDiv_vecNormSq_le
{A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ}
{v : Homogenization.Vec 2 → ℝ}
(hA : ContDiff ℝ (↑⊤) A)
(hv : ContDiff ℝ (↑⊤) v)
(x : Homogenization.Vec 2)
{D L : ℝ}
(hD : 0 ≤ D)
(hL : 0 ≤ L)
(hAj :
∀ (p : List (Fin 2)),
p.length ≤ 2 → ∀ (j k : Fin 2), |Section4.iterateMatrixWord A p x j k| ≤ D * ↑p.length.factorial * L ^ p.length)
:
Homogenization.vecNormSq (spaceGrad (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x) ≤ 14336 * D ^ 2 * ∑ w ∈ scWords2, (L ^ (2 - w.length)) ^ 2 * Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord w v) x)
Weighted pointwise bound:
|∇ ∇·(A ∇v)|² ≤ 14336 D² ∑_{|w| ≤ 2} L^{2(2-|w|)} |∇ ∂^w v|².