CompatibleFamily

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Compatible CoarseGraining families for an origin-cube coefficient

This internal bridge supplies CoarseGraining's family-valued interface from coefficient data on the origin cube. The chosen off-root extension remains confined to the existence proof; the frozen public A chooses only unique real scalars.

theorem Algsuperdiff.Section24.UnitCubeMultiscale.exists_compatibleTriadicCoeffFamily {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : ∃ (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a

Every coefficient on the origin cube is represented by at least one coherent CoarseGraining triadic family.

theorem Algsuperdiff.Section24.UnitCubeMultiscale.coeffOn_aeeq_of_root_aeeq {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (hG : (G.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {R : HCPolySupport.TriadicCube d} {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) : (F.coeffOn R).AEEq (G.coeffOn R)

Root a.e. agreement propagates to every descendant used by the root-local multiscale quantities.