WellDefinedness

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

Well-definedness of origin-cube lower multiscale ellipticity

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

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