WellDefinedness

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

Well-definedness of the origin-cube homogenization error

theorem Algsuperdiff.Section24.UnitCubeMultiscale.HomogenizationError.existsUnique {d : ℕ} (s : ℝ) (p q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (a0 : HCPolySupport.Mat d) : ∃! value : ℝ, ∀ (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a → value = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d 0) s p q F a0

The unique-value proof used by the frozen origin-cube homogenization-error anchor.