High-contrast homogenization: Entry.Source.CoarseSubadditivity

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

Countable source subadditivity

Near l.source.whitney. The accepted finite response defect and summability estimates give countable subadditivity after the relative volume weights have total mass one. Parent and pieces use one locally elliptic representative throughout each exhaustion. No coarse block is evaluated on a non-open remainder.

theorem HCPolySupport.HighContrast.Source.tsum_volumeRatio_eq_one {d : ℕ} {ι : Type u_1} {s : Set ι} (hs : s.Countable) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hmeas : ∀ i ∈ s, MeasurableSet (U i)) (hsub : ∀ i ∈ s, U i ⊆ W) (hdisj : s.PairwiseDisjoint U) (hnull : MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0) : ∑' (i : ↑s), (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal = 1

Countable relative volume weights have total mass one when the pieces cover a.e.

theorem HCPolySupport.HighContrast.Source.responseJ_le_tsum_of_partition {d : ℕ} {ι : Type u_1} {s : Set ι} (hs : s.Countable) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWopen : IsOpen W) (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hopen : ∀ i ∈ s, IsOpen (U i)) (hsub : ∀ i ∈ s, U i ⊆ W) (hdisj : s.PairwiseDisjoint U) (hnull : MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (p q : Vec d) : ResponseJ W p q a ≤ ∑' (i : ↑s), (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal * ResponseJ (U ↑i) p q a

Finite response defects vanish under an a.e. countable partition. The fixed ellipticity constants serve the parent and every piece in this proof.

theorem HCPolySupport.HighContrast.Source.quadratic_blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (blockScale c A) X) = c * (1 / 2 * blockVecDot X (blockMatVecMul A X))

Scalar dilation acts on the entire doubled quadratic form.

theorem HCPolySupport.HighContrast.Source.block_bound_of_response_partition {d : ℕ} {ι : Type u_1} {s : Set ι} (hs : s.Countable) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWopen : IsOpen W) (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hopen : ∀ i ∈ s, IsOpen (U i)) (hsub : ∀ i ∈ s, U i ⊆ W) (hdisj : s.PairwiseDisjoint U) (hnull : MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (A E : BlockMat d) (Ai : ι → BlockMat d) (c : ι → ℝ) (hA : ∀ (p q : Vec d), ResponseJ W p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul A (-p, q)) - vecDot p q) (hAi : ∀ i ∈ s, ∀ (p q : Vec d), ResponseJ (U i) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (Ai i) (-p, q)) - vecDot p q) (hc : Summable fun (i : ↑s) => (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal * c ↑i) (hb : ∀ i ∈ s, BlockMatLoewnerLE (Ai i) (blockScale (c i) E)) : BlockMatLoewnerLE A (blockScale (∑' (i : ↑s), (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal * c ↑i) E)

The mixed response identities and total volume mass turn a countable response partition into an every-vector block bound. This conditional bridge is discharged by the adapted coarse-block mixed response identity on the actual cells; it asserts no source estimate by itself.

theorem HCPolySupport.HighContrast.Source.coarseBlock_adapted_partition_bound {d : ℕ} [NeZero d] {ι : Type u_1} {s : Set ι} (hs : s.Countable) (q : Mat d) (hq : IsUnit q) (j : ℤ) (y : Vec d) (qi : ι → Mat d) (hqi : ∀ i ∈ s, IsUnit (qi i)) (ji : ι → ℤ) (yi : ι → Vec d) (a : CoeffSpace d) (E : BlockMat d) (c : ι → ℝ) : have W := adaptedCellTranslate q j y; have U := fun (i : ι) => adaptedCellTranslate (qi i) (ji i) (yi i); (∀ i ∈ s, U i ⊆ W) → s.PairwiseDisjoint U → MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0 → (Summable fun (i : ↑s) => (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal * c ↑i) → (∀ i ∈ s, BlockMatLoewnerLE (coarseBlock (U i) a) (blockScale (c i) E)) → BlockMatLoewnerLE (coarseBlock W a) (blockScale (∑' (i : ↑s), (MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal * c ↑i) E)

Countable subadditivity with a scalar reference bound, on the actual qualitative coefficient carrier and invertible adapted cells. Every response identity is supplied by the adapted coarse-block mixed response identity.

theorem HCPolySupport.HighContrast.Source.blockScale_le_blockScale_of_pos {d : ℕ} {E : BlockMat d} (hE : Book.Ch02.BlockPosDef E) {c c' : ℝ} (hc : c ≤ c') : BlockMatLoewnerLE (blockScale c E) (blockScale c' E)

Scaling a positive reference block is monotone in the real scalar, in the full quadratic order.

theorem HCPolySupport.HighContrast.Source.fullBlock_posSemidef_of_pos {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) (hpos : Book.Ch02.BlockPosDef A) : Matrix.PosSemidef (toFullBlockMat A)

Full block symmetry and positive quadratic form give the actual spectral positive-semidefinite matrix used by the Schatten norm.

theorem HCPolySupport.HighContrast.Source.blockTrace_le_of_order {d : ℕ} {A B : BlockMat d} (hAB : BlockMatLoewnerLE A B) : blockTrace A ≤ blockTrace B

Full quadratic order bounds the trace without assuming entrywise order.

theorem HCPolySupport.HighContrast.Source.blockOpNorm_le_scale_trace {d : ℕ} {A E : BlockMat d} {c : ℝ} (hA : IsSymmetricBlockMat A) (hpos : Book.Ch02.BlockPosDef A) (horder : BlockMatLoewnerLE A (blockScale c E)) : blockOpNorm A ≤ c * blockTrace E

Quadratic order on a positive full block controls its actual L2 operator norm.

theorem HCPolySupport.HighContrast.Source.summable_fullBlock_of_order {d : ℕ} {ι : Type u_1} (A : ι → BlockMat d) (E : BlockMat d) (w c : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hs : ∀ (i : ι), IsSymmetricBlockMat (A i)) (hp : ∀ (i : ι), Book.Ch02.BlockPosDef (A i)) (ho : ∀ (i : ι), BlockMatLoewnerLE (A i) (blockScale (c i) E)) (hc : Summable fun (i : ι) => w i * c i) : Summable fun (i : ι) => w i • toFullBlockMat (A i)

A summable positive scalar order envelope makes the actual full matrix series summable in the L2 operator topology.

theorem HCPolySupport.HighContrast.Source.quadratic_tsum_fullBlock {d : ℕ} {ι : Type u_1} (F : ι → FullBlockMat d) (hF : Summable F) (v : BlockVec d) : 1 / 2 * blockVecDot v (blockMatVecMul (ofFullBlockMat (∑' (i : ι), F i)) v) = ∑' (i : ι), 1 / 2 * blockVecDot v (blockMatVecMul (ofFullBlockMat (F i)) v)

Every-vector quadratic evaluation commutes with a convergent full matrix series; no replacement by scalar diagonal sums occurs.

theorem HCPolySupport.HighContrast.Source.isSymmetricBlockMat_tsum {d : ℕ} {ι : Type u_1} (F : ι → FullBlockMat d) (hF : Summable F) (hs : ∀ (i : ι), IsSymmetricBlockMat (ofFullBlockMat (F i))) : IsSymmetricBlockMat (ofFullBlockMat (∑' (i : ι), F i))

The full sum of symmetric matrices is symmetric in every pair of entries.

theorem HCPolySupport.HighContrast.Source.summable_quadratic_fullBlock {d : ℕ} {ι : Type u_1} (F : ι → FullBlockMat d) (hF : Summable F) (v : BlockVec d) : Summable fun (i : ι) => 1 / 2 * blockVecDot v (blockMatVecMul (ofFullBlockMat (F i)) v)

Every-vector quadratic evaluation commutes with a convergent full matrix series; no replacement by scalar diagonal sums occurs.

theorem HCPolySupport.HighContrast.Source.block_tsum_of_response_partition {d : ℕ} {ι : Type u_1} {s : Set ι} (hs : s.Countable) {W : Set (Vec d)} {U : ι → Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn W)] (hWopen : IsOpen W) (hWvol : (MeasureTheory.volume W).toReal ≠ 0) (hopen : ∀ i ∈ s, IsOpen (U i)) (hsub : ∀ i ∈ s, U i ⊆ W) (hdisj : s.PairwiseDisjoint U) (hnull : MeasureTheory.volume (W \ ⋃ i ∈ s, U i) = 0) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam W a) (A : BlockMat d) (Ai : ι → BlockMat d) (hA : ∀ (p q : Vec d), ResponseJ W p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul A (-p, q)) - vecDot p q) (hAi : ∀ i ∈ s, ∀ (p q : Vec d), ResponseJ (U i) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (Ai i) (-p, q)) - vecDot p q) (hseries : Summable fun (i : ↑s) => ((MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (Ai ↑i)) : BlockMatLoewnerLE A (ofFullBlockMat (∑' (i : ↑s), ((MeasureTheory.volume (U ↑i)).toReal / (MeasureTheory.volume W).toReal) • toFullBlockMat (Ai ↑i)))

The mixed response identity gives the actual full weighted block inequality. Total volume mass one is proved before the mixed terms cancel.

theorem HCPolySupport.HighContrast.Source.memLqSchatten_of_norm_envelope {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {N : ℝ} (hN : 1 ≤ N) {A : CoeffSpace d → BlockMat d} (hAm : HasMeasurableBlock P A) (hAs : ∀ᵐ (a : CoeffSpace d) ∂P, IsSymmetricBlockMat (A a)) {X : CoeffSpace d → ℝ} (hX : MeasureTheory.MemLp X (ENNReal.ofReal N) P) (D : ℝ) (hbound : ∀ᵐ (a : CoeffSpace d) ∂P, blockOpNorm (A a) ≤ D * X a) : SchattenMemLp P N A

A finite scalar operator-norm envelope gives the Schatten membership for symmetric full blocks, including matrix sums, differences and congruences.

theorem HCPolySupport.HighContrast.Source.full_matrix_series_envelope {d : ℕ} {ι : Type u_1} [Countable ι] (P : MeasureTheory.Measure (CoeffSpace d)) (F : ι → CoeffSpace d → FullBlockMat d) (hm : ∀ (i : ι), HasMeasurableBlock P fun (a : CoeffSpace d) => ofFullBlockMat (F i a)) (hs : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (i : ι), IsSymmetricBlockMat (ofFullBlockMat (F i a))) (c : ι → ℝ) (hc0 : ∀ (i : ι), 0 ≤ c i) (hc : Summable c) (X : CoeffSpace d → ℝ) (hX0 : ∀ (a : CoeffSpace d), 0 ≤ X a) (hb : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (i : ι), ‖F i a‖ ≤ c i * X a) : (∀ᵐ (a : CoeffSpace d) ∂P, Summable fun (i : ι) => F i a) ∧ (HasMeasurableBlock P fun (a : CoeffSpace d) => ofFullBlockMat (∑' (i : ι), F i a)) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, IsSymmetricBlockMat (ofFullBlockMat (∑' (i : ι), F i a))) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, ‖∑' (i : ι), F i a‖ ≤ (∑' (i : ι), c i) * X a) ∧ ∀ (s : Finset ι), (HasMeasurableBlock P fun (a : CoeffSpace d) => ofFullBlockMat (∑ i ∈ s, F i a)) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, IsSymmetricBlockMat (ofFullBlockMat (∑ i ∈ s, F i a))) ∧ ∀ᵐ (a : CoeffSpace d) ∂P, ‖∑ i ∈ s, F i a‖ ≤ (∑' (i : ι), c i) * X a

A common summable measurable envelope controls the actual full sum and all finite partial sums. Symmetry and measurability are established before moments.

theorem HCPolySupport.HighContrast.Source.lqSchatten_tsum_convergence {d : ℕ} {ι : Type u_1} [Countable ι] (P : MeasureTheory.Measure (CoeffSpace d)) (N : ℝ) (hN : 1 ≤ N) (F : ι → CoeffSpace d → FullBlockMat d) (hm : ∀ (i : ι), HasMeasurableBlock P fun (a : CoeffSpace d) => ofFullBlockMat (F i a)) (hs : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (i : ι), IsSymmetricBlockMat (ofFullBlockMat (F i a))) (c : ι → ℝ) (hc0 : ∀ (i : ι), 0 ≤ c i) (hc : Summable c) (X : CoeffSpace d → ℝ) (hX0 : ∀ (a : CoeffSpace d), 0 ≤ X a) (hX : MeasureTheory.MemLp X (ENNReal.ofReal N) P) (hb : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (i : ι), ‖F i a‖ ≤ c i * X a) : have M := fun (a : CoeffSpace d) => ofFullBlockMat (∑' (i : ι), F i a); have B := fun (s : Finset ι) (a : CoeffSpace d) => ofFullBlockMat (∑ i ∈ s, F i a); SchattenMemLp P N M ∧ (∀ (s : Finset ι), SchattenMemLp P N (B s) ∧ SchattenMemLp P N fun (a : CoeffSpace d) => blockSub (B s a) (M a)) ∧ Filter.Tendsto (fun (s : Finset ι) => lqSchattenNorm P N fun (a : CoeffSpace d) => blockSub (B s a) (M a)) Filter.atTop (nhds 0)

Dominated convergence in the actual L^N(S_N) norm for full matrix series. The sum, every partial sum and their differences have membership before their real norms are used. The common scalar envelope is integrable at N.