High-contrast homogenization: Provider.Entry.AdapterQuadratic

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

Quadratic forms of the weighted sums of a filling

e.two.grid.whitney.average is consumed against a majorant of every finite partial double sum of a filling's rows, and the majorant is presented as a doubled block. Its quadratic form has to be resolved into the rows and the remainder, and the resolution is the same at the pathwise and at the annealed level. The four elementary facts that do it are collected here: the passage from the Loewner order to the quadratic form, the resolution of a weighted double sum, the positivity of a finite sum of positive blocks, and the split of a partial sum at an intermediate scale.

Two arithmetic conveniences travel with them: a weighted row against a uniform bound on its cells, and the mean of an affine function of the source scale.

There are no definitions in this file.

Quadratic forms

theorem HCPolySupport.HighContrast.Entry.quad_le_of_le {d : ℕ} {A B : FullBlockMat d} (h : A ≤ B) (x : BlockCoord d → ℝ) : x ⬝ᵥ Matrix.mulVec A x ≤ x ⬝ᵥ Matrix.mulVec B x

The Loewner order on flattened blocks implies the order of the quadratic forms.

theorem HCPolySupport.HighContrast.Entry.blockQuadratic_double_sum {d : ℕ} (X : BlockVec d) (R : Finset ℤ) (Zf : ℤ → Finset (Fin d → ℤ)) (c : ℤ → (Fin d → ℤ) → ℝ) (A : ℤ → (Fin d → ℤ) → BlockMat d) (G : BlockMat d) : blockVecDot X (blockMatVecMul (ofFullBlockMat (∑ r ∈ R, ∑ w ∈ Zf r, c r w • toFullBlockMat (A r w) + toFullBlockMat G)) X) = ∑ r ∈ R, ∑ w ∈ Zf r, c r w * blockVecDot X (blockMatVecMul (A r w) X) + blockVecDot X (blockMatVecMul G X)

The quadratic form of a weighted double sum plus a remainder, resolved.

theorem HCPolySupport.HighContrast.Entry.half_blockQuadratic_majorant {d : ℕ} (X : BlockVec d) (R : Finset ℤ) (Zf : ℤ → Finset (Fin d → ℤ)) (c : ℤ → (Fin d → ℤ) → ℝ) (A : ℤ → (Fin d → ℤ) → BlockMat d) (cb : ℝ) (G : BlockMat d) : 1 / 2 * blockVecDot X (blockMatVecMul (ofFullBlockMat (∑ r ∈ R, ∑ w ∈ Zf r, c r w • toFullBlockMat (A r w) + cb • toFullBlockMat G)) X) = ∑ r ∈ R, ∑ w ∈ Zf r, c r w * (1 / 2 * blockVecDot X (blockMatVecMul (A r w) X)) + 1 / 2 * (cb * blockVecDot X (blockMatVecMul G X))

The majorant read through its half quadratic form, resolved into the rows and the scalar remainder. This is the shape in which e.two.grid.whitney.average compares its hypothesis.

theorem HCPolySupport.HighContrast.Entry.posSemidef_finsetSum {d : ℕ} {ι : Type u_1} {s : Finset ι} {A : ι → FullBlockMat d} (h : ∀ i ∈ s, Matrix.PosSemidef (A i)) : Matrix.PosSemidef (∑ i ∈ s, A i)

A finite sum of positive semidefinite flattened blocks is positive semidefinite.

Splitting a partial sum at an intermediate scale

theorem HCPolySupport.HighContrast.Entry.sum_Icc_le_of_belowStart {jStar n : ℤ} (hjn : jStar ≤ n) {row : ℤ → ℝ} {G : ℝ} (hrow0 : ∀ (r : ℤ), 0 ≤ row r) (hG0 : 0 ≤ G) (hbelow : ∀ (J' : ℤ), ∑ r ∈ Finset.Ico J' jStar, row r ≤ G) (J : ℤ) : ∑ r ∈ Finset.Icc J n, row r ≤ ∑ r ∈ Finset.Icc jStar n, row r + G

The printed split of the exhaustion hypothesis. A quantity dominating every partial sum below an intermediate scale, added to the part from that scale up, dominates every partial sum of the whole family.

A weighted row, and the mean of an affine function

theorem HCPolySupport.HighContrast.Entry.sum_weight_mul_le {d : ℕ} {ι : Type u_1} {Z : Finset ι} {V : ι → Set (Vec d)} {W : Set (Vec d)} {A : ι → ℝ} {B c : ℝ} (hB0 : 0 ≤ B) (hA : ∀ w ∈ Z, A w ≤ B) (hrow : ∑ w ∈ Z, (MeasureTheory.volume (V w)).toReal / (MeasureTheory.volume W).toReal ≤ c) : ∑ w ∈ Z, (MeasureTheory.volume (V w)).toReal / (MeasureTheory.volume W).toReal * A w ≤ c * B

A weighted row of a filling, against a uniform bound on its cells.

theorem HCPolySupport.HighContrast.Entry.integral_affine {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {S : CoeffSpace d → ℝ} (hS : MeasureTheory.Integrable S P) (al be : ℝ) : ∫ (a : CoeffSpace d), al + be * S a ∂P = al + be * ∫ (a : CoeffSpace d), S a ∂P

The mean of an affine function of the source scale.