ExistsUniqueUnitCubeBigLambda

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

theorem Algsuperdiff.Frozen.Section24.existsUnique_unitCubeBigLambda {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