Theorem: LipschitzWith.maxLog (Ray/Hartogs/MaxLog.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzWith (-b).exp.toNNReal (_root_.maxLog b)
Tactic:
rw [← lipschitzOn_univ]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Tactic:
have h := (LipschitzOnWith.log b).comp ((LipschitzWith.id.const_max b.exp).lipschitzOnWith univ)
  (by simp only [id_eq, Set.mapsTo_univ_iff, Set.mem_Ici, le_max_iff, le_refl, true_or,
    forall_const])
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Tactic:
have e : Real.log ∘ max (Real.exp b) = _root_.maxLog b := by funext x; simp [_root_.maxLog]
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
e : Real.log ∘ max b.exp = _root_.maxLog b
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
e : Real.log ∘ max b.exp = _root_.maxLog b
⊢ LipschitzOnWith (-b).exp.toNNReal (_root_.maxLog b) univ
Tactic:
simpa only [e, mul_one, id_eq, ge_iff_le, lipschitzOn_univ] using h
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Set.MapsTo (fun x => max b.exp (id x)) univ (Ici b.exp)
Tactic:
simp only [id_eq, Set.mapsTo_univ_iff, Set.mem_Ici, le_max_iff, le_refl, true_or,
forall_const]
State after:
no goals

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
⊢ Real.log ∘ max b.exp = _root_.maxLog b
Tactic:
funext x
State after:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
x : ℝ
⊢ (Real.log ∘ max b.exp) x = _root_.maxLog b x

State before:
case h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
h : LipschitzOnWith ((-b).exp.toNNReal * 1) (Real.log ∘ fun x => max b.exp (id x)) univ
x : ℝ
⊢ (Real.log ∘ max b.exp) x = _root_.maxLog b x
Tactic:
simp [_root_.maxLog]
State after:
no goals