Coarse-graining support: Support.Book.Ch02.Theorems.SubadditivityScalingDefinitions

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

structure HCPolySupport.Book.Ch02.DomainPartition {d : ℕ} (U : Domain d) : Type 1

Public triadic partition scaffold for the Chapter 2 subadditivity theorem.

The LaTeX statement is over triadic subcubes of a larger cube. The public Book-layer theorem keeps a small abstraction here, but the abstraction carries a triadic realization: cells enumerate descendants of one parent triadic cube, and the weights are the uniform \avsum weights from the notes.

• Cell : Type

  The index type enumerating the triadic cells of the partition.

• instFintype : Fintype self.Cell

  A finite enumeration of the partition's cell indices.

• cell : self.Cell → Domain d

  The open convex subdomain assigned to each partition cell index.

• cell_subset_parent (i : self.Cell) : (self.cell i).carrier ⊆ U.carrier
• weight : self.Cell → ℝ

  The uniform normalized weight of each triadic partition cell.

• weight_nonneg (i : self.Cell) : 0 ≤ self.weight i
• weight_sum_one : ∑ i : self.Cell, self.weight i = 1
• triadic_realization : ∃ (root : TriadicCube d) (depth : ℕ), U.carrier = openCubeSet root ∧ ∃ (e : self.Cell ≃ ↥(descendantsAtDepth root depth)), ∀ (i : self.Cell), (self.cell i).carrier = openCubeSet ↑(e i) ∧ self.weight i = (↑(Fintype.card self.Cell))⁻¹

noncomputable def HCPolySupport.Book.Ch02.DomainPartition.weightedAverage {d : ℕ} {U : Domain d} (P : DomainPartition U) (f : P.Cell → ℝ) : ℝ

Weighted average over the cells of a public finite partition.

Equations

• P.weightedAverage f = ∑ i : P.Cell, P.weight i * f i

noncomputable def HCPolySupport.Book.Ch02.DomainPartition.weightedMatAverage {d : ℕ} {U : Domain d} (P : DomainPartition U) (F : P.Cell → Mat d) : Mat d

Weighted matrix average over the cells of a public finite partition.

Equations

• P.weightedMatAverage F i j = P.weightedAverage fun (c : P.Cell) => F c i j

noncomputable def HCPolySupport.Book.Ch02.DomainPartition.weightedBlockAverage {d : ℕ} {U : Domain d} (P : DomainPartition U) (F : P.Cell → BlockMat d) : BlockMat d

Weighted block-matrix average over the cells of a public finite partition.

Equations

• One or more equations did not get rendered due to their size.

structure HCPolySupport.Book.Ch02.ResponseSubadditivityAndScalingTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : Prop

Public theorem package for l.cg.subadditivity.basic.definitions.

Coefficient rescaling is stated a.e. by CoeffOn.AEScaled, not by pointwise equality of representatives. The canonical public theorem proving this package is responseSubadditivityAndScalingTheory in SubadditivityScaling.lean.

• responseJ_subadditive (P : DomainPartition U) (aCell : (i : P.Cell) → CoeffOn (P.cell i)) (_hCell : ∀ (i : P.Cell), a.RestrictsTo (aCell i)) (p q : Vec d) : responseJ U a p q ≤ P.weightedAverage fun (i : P.Cell) => responseJ (P.cell i) (aCell i) p q
• responseJ_homogeneous {lam : ℝ} : 0 < lam → ∀ {b : CoeffOn U}, CoeffOn.AEScaled lam a b → ∀ (p q : Vec d), responseJ U b p q = responseJ U a (√lam • p) ((√lam)⁻¹ • q)
• sigma_homogeneous {lam : ℝ} : 0 < lam → ∀ {b : CoeffOn U}, CoeffOn.AEScaled lam a b → sigmaCoarse U b = lam • sigmaCoarse U a
• sigmaStar_homogeneous {lam : ℝ} : 0 < lam → ∀ {b : CoeffOn U}, CoeffOn.AEScaled lam a b → sigmaStarCoarse U b = lam • sigmaStarCoarse U a
• kappa_homogeneous {lam : ℝ} : 0 < lam → ∀ {b : CoeffOn U}, CoeffOn.AEScaled lam a b → kappaCoarse U b = lam • kappaCoarse U a