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

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

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

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