Theorem: Minimization.Relaxation.induces_original_problem_optimality (CvxLean/Lib/Relaxation.lean)

State before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
⊢ p.optimal (phi_inv y)
Tactic:
refine ⟨h_feas_y, ?_⟩
State after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
⊢ ∀ (y_1 : D), p.feasible y_1 → p.objFun (phi_inv y) ≤ p.objFun y_1

State before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
⊢ ∀ (y_1 : D), p.feasible y_1 → p.objFun (phi_inv y) ≤ p.objFun y_1
Tactic:
intros x h_feas_x
State after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ p.objFun (phi_inv y) ≤ p.objFun x

State before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ p.objFun (phi_inv y) ≤ p.objFun x
Tactic:
rw [h_objFun _ h_feas_y, phi_left_inv]
State after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ q.objFun y ≤ p.objFun x

State before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
⊢ q.objFun y ≤ p.objFun x
Tactic:
have h_bound := h_opt_y.2 (Rx.phi x) (Rx.phi_feasibility x h_feas_x)
State after:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
h_bound : q.objFun y ≤ q.objFun (Rx.phi x)
⊢ q.objFun y ≤ p.objFun x

State before:
D E F R : Type
inst✝ : Preorder R
p : Minimization D R
q : Minimization E R
r : Minimization F R
Rx : p.Relaxation q
phi_inv : E → D
phi_left_inv : Function.LeftInverse Rx.phi phi_inv
h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)
y : E
h_opt_y : q.optimal y
h_feas_y : p.feasible (phi_inv y)
x : D
h_feas_x : p.feasible x
h_bound : q.objFun y ≤ q.objFun (Rx.phi x)
⊢ q.objFun y ≤ p.objFun x
Tactic:
rwa [← h_objFun _ h_feas_x] at h_bound
State after:
no goals