Theorem: Smt.Reconstruct.Arith.arithTransExpApproxAboveNeg (Smt/Reconstruct/Arith/TransFns/ArithTransExpApproxAboveNeg.lean)

State before:
d : ℕ
l u t : ℝ
⊢ let p := taylorWithinEval Real.exp d (Set.Ioo l u) 0;
  let secant := (p l - p u) / (l - u) * (t - l) + p l;
  StrictConvexOn ℝ (Set.Icc l u) p → t < 0 → t > l ∧ t < u → t.exp ≤ secant
Tactic:
rintro p secant p_conv t_neg ⟨l_bound, u_bound⟩
State after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
⊢ t.exp ≤ secant

State before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
⊢ t.exp ≤ secant
Tactic:
have lLeT : l ≤ t := LT.lt.le l_bound
State after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
⊢ t.exp ≤ secant

State before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
⊢ t.exp ≤ secant
Tactic:
have tLeU : t ≤ u := LT.lt.le u_bound
State after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
⊢ t.exp ≤ secant

State before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
⊢ t.exp ≤ secant
Tactic:
have lLeU : l ≤ u := LE.le.trans lLeT tLeU
State after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
⊢ t.exp ≤ secant

State before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
⊢ t.exp ≤ secant
Tactic:
have lLtU : l < u := LT.lt.trans l_bound u_bound
State after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
⊢ t.exp ≤ secant

State before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
⊢ t.exp ≤ secant
Tactic:
have conv_imples: (p l - p t) / (l - t) < (p u - p t) / (u - t) :=
  StrictConvexOn.secant_strict_mono p_conv (a := t) (x := l) (y := u)
    (Set.mem_Icc.mpr ⟨lLeT, tLeU⟩)
    (Set.left_mem_Icc.mpr lLeU)
    (Set.right_mem_Icc.mpr lLeU)
    (ne_of_lt l_bound) (Ne.symm (ne_of_lt u_bound)) lLtU
State after:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
conv_imples : (p l - p t) / (l - t) < (p u - p t) / (u - t)
⊢ t.exp ≤ secant

State before:
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
lLtU : l < u
conv_imples : (p l - p t) / (l - t) < (p u - p t) / (u - t)
⊢ t.exp ≤ secant
Tactic:
admit
State after:
no goals