Documentation

CvxLean.Lib.Equivalence

Equivalence of optimization problems #

We define equivalence and strong equivalence, and several equivalence-preserving transformations.

References #

structure Minimization.Equivalence {D : Type} {E : Type} {R : Type} [Preorder R] (p : Minimization D R) (q : Minimization E R) :

Regular notion of equivalence between optimization problems. We require maps (φ, ψ) between teh domains of p and q such that they map optimal points to optimal points.

  • phi : DE
  • psi : ED
  • phi_optimality : ∀ (x : D), p.optimal xq.optimal (self.phi x)
  • psi_optimality : ∀ (x : E), q.optimal xp.optimal (self.psi x)
Instances For
    theorem Minimization.Equivalence.phi_optimality {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.Equivalence q) (x : D) :
    p.optimal xq.optimal (self.phi x)
    theorem Minimization.Equivalence.psi_optimality {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.Equivalence q) (x : E) :
    q.optimal xp.optimal (self.psi x)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Minimization.Equivalence.refl {D : Type} {R : Type} [Preorder R] {p : Minimization D R} :
      p.Equivalence p
      Equations
      • Minimization.Equivalence.refl = { phi := id, psi := id, phi_optimality := , psi_optimality := }
      Instances For
        def Minimization.Equivalence.symm {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E✝ R} (E : p.Equivalence q) :
        q.Equivalence p
        Equations
        • E.symm = { phi := E.psi, psi := E.phi, phi_optimality := , psi_optimality := }
        Instances For
          def Minimization.Equivalence.trans {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} {r : Minimization F R} (E₁ : p.Equivalence q) (E₂ : q.Equivalence r) :
          p.Equivalence r
          Equations
          • E₁.trans E₂ = { phi := E₂.phi E₁.phi, psi := E₁.psi E₂.psi, phi_optimality := , psi_optimality := }
          Instances For
            instance Minimization.Equivalence.instTrans {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] :
            Trans Minimization.Equivalence Minimization.Equivalence Minimization.Equivalence
            Equations
            def Minimization.Equivalence.toFwd {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E✝ R} (E : p.Equivalence q) :
            p.Solutionq.Solution

            An equivalence induces a map between the solution set of p and the solution set of q.

            Equations
            • E.toFwd sol = { point := E.phi sol.point, isOptimal := }
            Instances For
              def Minimization.Equivalence.toBwd {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E✝ R} (E : p.Equivalence q) :
              q.Solutionp.Solution

              An equivalence induces a map between the solution set of q and the solution set of p.

              Equations
              • E.toBwd sol = { point := E.psi sol.point, isOptimal := }
              Instances For
                structure Minimization.StrongEquivalence {D : Type} {E : Type} {R : Type} [Preorder R] (p : Minimization D R) (q : Minimization E R) :

                Notion of equivalence used by the DCP procedure. It makes some proofs simpler. The optimality-preserving requirements of (φ, ψ) are replaced by:

                • for every p-feasible x, g(φ(x)) ≤ f(x), i.e. φ gives a lower bound of f.
                • for every q-feasible y, f(ψ(y)) ≤ g(y), i.e. ψ fives a lower bound of g.
                • phi : DE
                • psi : ED
                • phi_feasibility : ∀ (x : D), p.feasible xq.feasible (self.phi x)
                • psi_feasibility : ∀ (y : E), q.feasible yp.feasible (self.psi y)
                • phi_optimality : ∀ (x : D), p.feasible xq.objFun (self.phi x) p.objFun x
                • psi_optimality : ∀ (y : E), q.feasible yp.objFun (self.psi y) q.objFun y
                Instances For
                  theorem Minimization.StrongEquivalence.phi_feasibility {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.StrongEquivalence q) (x : D) :
                  p.feasible xq.feasible (self.phi x)
                  theorem Minimization.StrongEquivalence.psi_feasibility {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.StrongEquivalence q) (y : E) :
                  q.feasible yp.feasible (self.psi y)
                  theorem Minimization.StrongEquivalence.phi_optimality {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.StrongEquivalence q) (x : D) :
                  p.feasible xq.objFun (self.phi x) p.objFun x
                  theorem Minimization.StrongEquivalence.psi_optimality {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.StrongEquivalence q) (y : E) :
                  q.feasible yp.objFun (self.psi y) q.objFun y
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Minimization.StrongEquivalence.refl {D : Type} {R : Type} [Preorder R] {p : Minimization D R} :
                    p.StrongEquivalence p
                    Equations
                    • Minimization.StrongEquivalence.refl = { phi := id, psi := id, phi_feasibility := , psi_feasibility := , phi_optimality := , psi_optimality := }
                    Instances For
                      def Minimization.StrongEquivalence.symm {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E✝ R} (E : p.StrongEquivalence q) :
                      q.StrongEquivalence p
                      Equations
                      • E.symm = { phi := E.psi, psi := E.phi, phi_feasibility := , psi_feasibility := , phi_optimality := , psi_optimality := }
                      Instances For
                        def Minimization.StrongEquivalence.trans {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} {r : Minimization F R} (E₁ : p.StrongEquivalence q) (E₂ : q.StrongEquivalence r) :
                        p.StrongEquivalence r
                        Equations
                        • E₁.trans E₂ = { phi := E₂.phi E₁.phi, psi := E₁.psi E₂.psi, phi_feasibility := , psi_feasibility := , phi_optimality := , psi_optimality := }
                        Instances For
                          instance Minimization.StrongEquivalence.instTrans {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] :
                          Trans Minimization.StrongEquivalence Minimization.StrongEquivalence Minimization.StrongEquivalence
                          Equations
                          def Minimization.Equivalence.ofEq {D : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization D R} (h : p = q) :
                          p.Equivalence q

                          Equal problems are equivalent. Note that the domain needs to be the same. We intentionally do not define this as h ▸ Equivalence.refl (p := p) so that phi and psi can be easily extracted.

                          Equations
                          Instances For
                            def Minimization.Equivalence.ofStrongEquivalence {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E✝ R} (E : p.StrongEquivalence q) :
                            p.Equivalence q

                            As expected, an Equivalence can be built from a StrongEquivalence.

                            Equations
                            Instances For
                              instance Minimization.Equivalence.instTransStrongEquivalence {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] :
                              Trans Minimization.StrongEquivalence Minimization.Equivalence Minimization.Equivalence
                              Equations
                              • One or more equations did not get rendered due to their size.
                              instance Minimization.Equivalence.instTransStrongEquivalence_1 {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] :
                              Trans Minimization.Equivalence Minimization.StrongEquivalence Minimization.Equivalence
                              Equations
                              • One or more equations did not get rendered due to their size.
                              def Minimization.StrongEquivalence.toFwd {D : Type} {E : Type} {R : Type} [Preorder R] (p : Minimization D R) (q : Minimization E✝ R) (E : p.StrongEquivalence q) :
                              p.Solutionq.Solution
                              Equations
                              Instances For
                                def Minimization.StrongEquivalence.toBwd {D : Type} {E : Type} {R : Type} [Preorder R] (p : Minimization D R) (q : Minimization E✝ R) (E : p.StrongEquivalence q) :
                                q.Solutionp.Solution
                                Equations
                                Instances For

                                  Mapping the objective function by monotonic functions yields an equivalence. Also, mapping the whole domain by a function with a right inverse.

                                  def Minimization.Equivalence.map_objFun {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {g : RR} (h : ∀ {r s : D}, cs rcs s(g (f r) g (f s) f r f s)) :
                                  { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : D) => g (f x), constraints := cs }

                                  See [BV04,p.131] where g is ψ₀.

                                  Equations
                                  Instances For
                                    noncomputable def Minimization.Equivalence.map_objFun_log {D : Type} {cs : DProp} {f : D} (h : ∀ (x : D), cs xf x > 0) :
                                    { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : D) => (f x).log, constraints := cs }
                                    Equations
                                    Instances For
                                      noncomputable def Minimization.Equivalence.map_objFun_sq {D : Type} {cs : DProp} {f : D} (h : ∀ (x : D), cs xf x 0) :
                                      { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : D) => f x ^ 2, constraints := cs }
                                      Equations
                                      Instances For
                                        def Minimization.Equivalence.map_domain {D : Type} {E : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {fwd : DE} {bwd : ED} (h : ∀ (x : D), cs xbwd (fwd x) = x) :
                                        { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : E) => f (bwd x), constraints := fun (x : E) => cs (bwd x) }

                                        This is simply a change of variables, see ChangeOfVariables.toEquivalence and [BV04,p.130].

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Rewriting the objective function or the constraints leads to equivalent problems.

                                          We assume constraints are joind by . A problem with several constraints can be written as ⟨f, [[c1, ..., cn]]⟩.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def Minimization.Equivalence.rewrite_objFun {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {g : DR} (hrw : ∀ (x : D), cs xf x = g x) :
                                            { objFun := f, constraints := cs }.Equivalence { objFun := g, constraints := cs }
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Minimization.Equivalence.rewrite_objFun_1 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xf x = g x) :
                                              { objFun := f, constraints := c1 }.Equivalence { objFun := g, constraints := c1 }
                                              Equations
                                              Instances For
                                                def Minimization.Equivalence.rewrite_objFun_2 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xf x = g x) :
                                                { objFun := f, constraints := fun (x : D) => c1 x c2 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x }
                                                Equations
                                                Instances For
                                                  def Minimization.Equivalence.rewrite_objFun_3 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xf x = g x) :
                                                  { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x }
                                                  Equations
                                                  Instances For
                                                    def Minimization.Equivalence.rewrite_objFun_4 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xf x = g x) :
                                                    { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x }
                                                    Equations
                                                    Instances For
                                                      def Minimization.Equivalence.rewrite_objFun_5 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xf x = g x) :
                                                      { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x }
                                                      Equations
                                                      Instances For
                                                        def Minimization.Equivalence.rewrite_objFun_6 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xf x = g x) :
                                                        { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x }
                                                        Equations
                                                        Instances For
                                                          def Minimization.Equivalence.rewrite_objFun_7 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xf x = g x) :
                                                          { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x }
                                                          Equations
                                                          Instances For
                                                            def Minimization.Equivalence.rewrite_objFun_8 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xf x = g x) :
                                                            { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x }
                                                            Equations
                                                            Instances For
                                                              def Minimization.Equivalence.rewrite_objFun_9 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c9 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 xf x = g x) :
                                                              { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x }
                                                              Equations
                                                              Instances For
                                                                def Minimization.Equivalence.rewrite_objFun_10 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c9 : DProp} {c10 : DProp} {g : DR} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 xc10 xf x = g x) :
                                                                { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x c10 x }.Equivalence { objFun := g, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x c10 x }
                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        def Minimization.Equivalence.rewrite_constraints {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {cs' : DProp} (hrw : ∀ (x : D), cs x cs' x) :
                                                                        { objFun := f, constraints := fun (x : D) => cs x }.Equivalence { objFun := f, constraints := fun (x : D) => cs' x }
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          def Minimization.Equivalence.rewrite_constraint_1 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c1' : DProp} {cs : DProp} (hrw : ∀ (x : D), cs x(c1 x c1' x)) :
                                                                          { objFun := f, constraints := fun (x : D) => c1 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1' x cs x }
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            def Minimization.Equivalence.rewrite_constraint_1_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c1' : DProp} (hrw : ∀ (x : D), c1 x c1' x) :
                                                                            { objFun := f, constraints := fun (x : D) => c1 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1' x }
                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Minimization.Equivalence.rewrite_constraint_2 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c2' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xcs x(c2 x c2' x)) :
                                                                              { objFun := f, constraints := fun (x : D) => c1 x c2 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2' x cs x }
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                def Minimization.Equivalence.rewrite_constraint_2_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c2' : DProp} (hrw : ∀ (x : D), c1 x(c2 x c2' x)) :
                                                                                { objFun := f, constraints := fun (x : D) => c1 x c2 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2' x }
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  def Minimization.Equivalence.rewrite_constraint_3 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c3' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xcs x(c3 x c3' x)) :
                                                                                  { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3' x cs x }
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    def Minimization.Equivalence.rewrite_constraint_3_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c3' : DProp} (hrw : ∀ (x : D), c1 xc2 x(c3 x c3' x)) :
                                                                                    { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3' x }
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def Minimization.Equivalence.rewrite_constraint_4 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c4' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xcs x(c4 x c4' x)) :
                                                                                      { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4' x cs x }
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        def Minimization.Equivalence.rewrite_constraint_4_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c4' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 x(c4 x c4' x)) :
                                                                                        { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4' x }
                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          def Minimization.Equivalence.rewrite_constraint_5 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c5' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xcs x(c5 x c5' x)) :
                                                                                          { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5' x cs x }
                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            def Minimization.Equivalence.rewrite_constraint_5_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c5' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 x(c5 x c5' x)) :
                                                                                            { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5' x }
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              def Minimization.Equivalence.rewrite_constraint_6 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c6' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xcs x(c6 x c6' x)) :
                                                                                              { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6' x cs x }
                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                def Minimization.Equivalence.rewrite_constraint_6_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c6' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 x(c6 x c6' x)) :
                                                                                                { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6' x }
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  def Minimization.Equivalence.rewrite_constraint_7 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c7' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xcs x(c7 x c7' x)) :
                                                                                                  { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7' x cs x }
                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    def Minimization.Equivalence.rewrite_constraint_7_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c7' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 x(c7 x c7' x)) :
                                                                                                    { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7' x }
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      def Minimization.Equivalence.rewrite_constraint_8 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c8' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xcs x(c8 x c8' x)) :
                                                                                                      { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8' x cs x }
                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        def Minimization.Equivalence.rewrite_constraint_8_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c8' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 x(c8 x c8' x)) :
                                                                                                        { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8' x }
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          def Minimization.Equivalence.rewrite_constraint_9 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c9 : DProp} {c9' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xcs x(c9 x c9' x)) :
                                                                                                          { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x cs x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9' x cs x }
                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            def Minimization.Equivalence.rewrite_constraint_9_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c9 : DProp} {c9' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 x(c9 x c9' x)) :
                                                                                                            { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9' x }
                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              def Minimization.Equivalence.rewrite_constraint_10 {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c9 : DProp} {c10 : DProp} {c10' : DProp} {cs : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 xcs x(c10 x c10' x)) :
                                                                                                              { objFun := f, constraints := fun (x : D) => c1 x (fun (x : D) => c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x c10 x cs x) x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x (fun (x : D) => c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x c10' x cs x) x }
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                def Minimization.Equivalence.rewrite_constraint_10_last {D : Type} {R : Type} [Preorder R] {f : DR} {c1 : DProp} {c2 : DProp} {c3 : DProp} {c4 : DProp} {c5 : DProp} {c6 : DProp} {c7 : DProp} {c8 : DProp} {c9 : DProp} {c10 : DProp} {c10' : DProp} (hrw : ∀ (x : D), c1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 x(c10 x c10' x)) :
                                                                                                                { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x c10 x }.Equivalence { objFun := f, constraints := fun (x : D) => c1 x c2 x c3 x c4 x c5 x c6 x c7 x c8 x c9 x c10' x }
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For

                                                                                                                  Other equivalence-preserving transformations. These are not used by any tactic but can be used directly. They provide evidence that our notion of equivalence captures the expected transformations.

                                                                                                                  def Minimization.Equivalence.add_constraint {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {cs' : DProp} (h : ∀ (x : D), cs xcs' x) :
                                                                                                                  { objFun := f, constraints := cs }.Equivalence { objFun := f, constraints := fun (x : D) => cs' x cs x }

                                                                                                                  We can always add a redundant constraint. This might be useful to help the reduction algorithm infer some constraints that cannot be easily infered by arith.

                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    def Minimization.Equivalence.map_le_constraint_standard_form {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} [Zero R] {cs' : DProp} {fi : DR} {g : RR} (hcs : ∀ (x : D), cs x fi x 0 cs' x) (hg : ∀ (x : R), g x 0 x 0) :
                                                                                                                    { objFun := f, constraints := cs }.Equivalence { objFun := f, constraints := fun (x : D) => g (fi x) 0 cs' x }

                                                                                                                    See [BV04,p.131] where g is ψᵢ.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      def Minimization.Equivalence.map_eq_constraint_standard_form {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} [Zero R] {cs' : DProp} {hi : DR} {g : RR} (hcs : ∀ (x : D), cs x hi x = 0 cs' x) (hg : ∀ (x : R), g x = 0 x = 0) :
                                                                                                                      { objFun := f, constraints := cs }.Equivalence { objFun := f, constraints := fun (x : D) => g (hi x) = 0 cs' x }

                                                                                                                      See [BV04,p.131] where g is ψₘ₊ᵢ.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        def Minimization.Equivalence.add_slack_variable_standard_form {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {cs' : DProp} {fi : D} (hcs : ∀ (x : D), cs x fi x 0 cs' x) :
                                                                                                                        { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : × D) => match x with | (fst, x) => f x, constraints := fun (x : × D) => match x with | (si, x) => 0 si fi x + si = 0 cs' x }

                                                                                                                        Adding a slack variable [BV04,p.131].

                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For
                                                                                                                          noncomputable def Minimization.Equivalence.eliminate_eq_constraint_standard_form {D : Type} {E : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} [Inhabited E] {cs' : DProp} {hi : D} {g : ED} (hcs : ∀ (x : D), cs x hi x = 0 cs' x) (hg : ∀ (x : D), hi x = 0 ∃ (z : E), x = g z) :
                                                                                                                          { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : E) => f (g x), constraints := fun (x : E) => cs' (g x) }

                                                                                                                          Eliminate equality constraints [BV04,p.132].

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            def Minimization.Equivalence.decompose_constraint {D : Type} {E : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} (g : DE) (cs' : DEProp) (hc : ∀ (x : D), cs x cs' x (g x)) :
                                                                                                                            { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : D × E) => match x with | (x, snd) => f x, constraints := fun (x : D × E) => match x with | (x, y) => y = g x cs' x y }

                                                                                                                            Decompose constraint by introducing another equality constraint [BV04,p.132].

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              def Minimization.Equivalence.epigraph_form {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} :
                                                                                                                              { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : R × D) => match x with | (t, snd) => t, constraints := fun (x : R × D) => match x with | (t, x) => f x t cs x }

                                                                                                                              Epigraph form [BV04,p.134].

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                def Minimization.Equivalence.eq_to_le_left {D : Type} {E : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type u_1} [Preorder S] (e : D S × E) (g : ES) (cs' : DProp) (hcs : ∀ {x : D}, cs x (e x).1 = g (e x).2 cs' x) (hf : ∀ (y : E) (r s : S), f (e.symm (r, y)) = f (e.symm (s, y))) (h_mono : ∀ (y : E) (r s : S), r scs' (e.symm (r, y))cs' (e.symm (s, y))) :
                                                                                                                                { objFun := f, constraints := cs }.Equivalence { objFun := f, constraints := fun (x : D) => (e x).1 g (e x).2 cs' x }

                                                                                                                                Suppose D ≃ S × E. Let problem p := ⟨f, cs⟩ be defined over D. Every x : D maps one-to-one to (s, y) : S × E. Assume that x is p-feasible iff s = g y and cs' x. We can think of s as a new variable. If changing s does not change the objective function and the new constraints c respect monotonicity in S, we have that p is equivalent to the problem ⟨f, s ≤ g y ∧ cs' x⟩.

                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  def Minimization.Equivalence.eq_to_le_right {D : Type} {E : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type u_1} [Preorder S] (e : D S × E) (g : ES) (cs' : DProp) (hcs : ∀ {x : D}, cs x g (e x).2 = (e x).1 cs' x) (hf : ∀ (x : E) (r s : S), f (e.symm (r, x)) = f (e.symm (s, x))) (h_mono : ∀ (x : E) (r s : S), r scs' (e.symm (s, x))cs' (e.symm (r, x))) :
                                                                                                                                  { objFun := f, constraints := cs }.Equivalence { objFun := f, constraints := fun (x : D) => g (e x).2 (e x).1 cs' x }

                                                                                                                                  Similar to eq_to_le_left with the monotonicity condition on c flipped. In this case we have that P is equivalent to ⟨f, g y ≤ s ∧ cs' x⟩.

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    def Minimization.Equivalence.domain_equiv {D : Type} {E : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} (e : E D) :
                                                                                                                                    { objFun := f, constraints := cs }.Equivalence { objFun := f e, constraints := cs e }

                                                                                                                                    Changing the domain to an equivalent type yields an equivalent problem.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      def Minimization.Equivalence.linearization_mono {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type} [Preorder S] (g : DS) (c : SDProp) (h : SDR) (hf : ∀ (x : D), f x = h (g x) x) (hcs : ∀ (x : D), cs x = c (g x) x) (h_mono_f : ∀ (x : D) (r s : S), r sh s x h r x) (h_mono_cs : ∀ (x : D) (r s : S), r sc r xc s x) :
                                                                                                                                      { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : S × D) => match x with | (s, y) => h s y, constraints := fun (x : S × D) => match x with | (s, y) => s g y c s y }

                                                                                                                                      Introduce a new variable s that replaces occurrences of (non-linear) g x in the original problem. The resulting problem has an extra constraint s ≤ g y. The objective funciton and the rest of the constraints need to satisfy the appropriate monotonicity conditions [Gra05,4.2.1].

                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        def Minimization.Equivalence.linearization_antimono {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type} [Preorder S] (g : DS) (c : SDProp) (h : SDR) (hf : ∀ (x : D), f x = h (g x) x) (hcs : ∀ (x : D), cs x = c (g x) x) (h_mono_f : ∀ (x : D) (r s : S), r sh r x h s x) (h_mono_cs : ∀ (x : D) (r s : S), r sc s xc r x) :
                                                                                                                                        { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : S × D) => match x with | (s, y) => h s y, constraints := fun (x : S × D) => match x with | (s, y) => g y s c s y }

                                                                                                                                        Similar to linearization_mono with the monotonicity conditions flipped. The resulting problem adds the exactra constraint g y ≤ s in this case [Gra05,4.2.1].

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          def Minimization.Equivalence.graph_expansion_greatest {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type} [Preorder S] (g : DS) (c : SDProp) (d : SDProp) (h : SDR) (hg : ∀ (x : D) (v : S), c v xIsGreatest {y : S | d y x} (g x)) (hf : ∀ (x : D), f x = h (g x) x) (hcs : ∀ (x : D), cs x = c (g x) x) (h_mono_f : ∀ (x : D) (r s : S), r sh s x h r x) (h_mono_cs : ∀ (x : D) (r s : S), r sc r xc s x) :
                                                                                                                                          { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : S × D) => match x with | (s, y) => h s y, constraints := fun (x : S × D) => match x with | (s, y) => d s y c s y }

                                                                                                                                          This can be seen as a generalization of linearization_mono, where d is the graph implementation of g. This is not used by the DCP procedure.

                                                                                                                                          Equations
                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                          Instances For
                                                                                                                                            def Minimization.Equivalence.graph_expansion_least {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type} [Preorder S] (g : DS) (c : SDProp) (d : SDProp) (h : SDR) (hg : ∀ (x : D) (v : S), c v xIsLeast {y : S | d y x} (g x)) (hf : ∀ (x : D), f x = h (g x) x) (hcs : ∀ (x : D), cs x = c (g x) x) (h_mono_f : ∀ (x : D) (r s : S), r sh r x h s x) (h_mono_cs : ∀ (x : D) (r s : S), r sc s xc r x) :
                                                                                                                                            { objFun := f, constraints := cs }.Equivalence { objFun := fun (x : S × D) => match x with | (s, y) => h s y, constraints := fun (x : S × D) => match x with | (s, y) => d s y c s y }

                                                                                                                                            Similar to graph_expansion_greatest but in the flipped monotonicity context, c.f. linearization_antimono. This is not used by the DCP procedure.

                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For
                                                                                                                                              def Minimization.Equivalence.graph_expansion_least_forall {D : Type} {R : Type} [Preorder R] {f : DR} {cs : DProp} {S : Type} {I : Type} [Preorder S] [Inhabited I] (g : DIS) (c : SDProp) (d : SDProp) (hg : ∀ (x : D) (v : S) (i : I), c v xIsLeast {y : S | d y x} (g x i)) (hcs : ∀ (x : D), cs x = ∀ (i : I), c (g x i) x) (h_mono_cs : ∀ (x : D) (r s : S), r sc s xc r x) :
                                                                                                                                              { objFun := f, constraints := cs }.Equivalence { objFun := fun (sy : (IS) × D) => f sy.2, constraints := fun (sy : (IS) × D) => (∀ (i : I), d (sy.1 i) sy.2) ∀ (i : I), c (sy.1 i) sy.2 }

                                                                                                                                              Version of graph_expansion_least that works with vectors.

                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For