Commit 2023-02-20 12:18 c2ba2044

View on Github →

feat: Port Data.QPF.Multivariate.Basic (#2223)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/QPF/Multivariate/Basic.lean

added def MvQPF.IsUniform

added def MvQPF.LiftPPreservation

added def MvQPF.SuppPreservation

added theorem MvQPF.comp_map

added theorem MvQPF.has_good_supp_iff

added theorem MvQPF.liftP_iff

added theorem MvQPF.liftP_iff_of_isUniform

added theorem MvQPF.liftR_iff

added theorem MvQPF.liftpPreservation_iff_uniform

added theorem MvQPF.mem_supp

added theorem MvQPF.suppPreservation_iff_isUniform

added theorem MvQPF.suppPreservation_iff_liftpPreservation

added theorem MvQPF.supp_eq

added theorem MvQPF.supp_eq_of_isUniform

added theorem MvQPF.supp_map