-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem dist_next_apply_le_of_le {f₁ f₂ : FunSpace v} {n : ℕ} {d : ℝ}
    (h : ∀ t, dist (f₁ t) (f₂ t) ≤ (v.L * |t.1 - v.t₀|) ^ n / n ! * d) (t : Icc v.tMin v.tMax) :
    dist (next f₁ t) (next f₂ t) ≤ (v.L * |t.1 - v.t₀|) ^ (n + 1) / (n + 1)! * d

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (↑v.t₀ ⊓ ↑t) (↑v.t₀ ⊔ ↑t)
⊢ ‖f₁.vComp τ - f₂.vComp τ‖ ≤ ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)

Tactic:
refine (v.lipschitzOnWith (v.proj τ).2).norm_sub_le_of_le (f₁.mem_closedBall _)
    (f₂.mem_closedBall _) ((h _).trans_eq ?_)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (↑v.t₀ ⊓ ↑t) (↑v.t₀ ⊔ ↑t)
⊢ (↑v.L * |↑(v.proj τ) - ↑v.t₀|) ^ n / ↑n ! * d = (↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d) =
    (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d

Tactic:
simp_rw [mul_pow, div_eq_mul_inv, mul_assoc, MeasureTheory.integral_mul_left,
  MeasureTheory.integral_mul_right, integral_pow_abs_sub_uIoc, div_eq_mul_inv,
  pow_succ' (v.L : ℝ), Nat.factorial_succ, Nat.cast_mul, Nat.cast_succ, mul_inv, mul_assoc]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (↑v.t₀ ⊓ ↑t) (↑v.t₀ ⊔ ↑t)
⊢ (↑v.L * |↑(v.proj τ) - ↑v.t₀|) ^ n / ↑n ! * d = (↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d

Tactic:
rw [v.proj_of_mem]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (↑v.t₀ ⊓ ↑t) (↑v.t₀ ⊔ ↑t)
⊢ τ ∈ Icc v.tMin v.tMax

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
h : ∀ (t : ↑(Icc v.tMin v.tMax)), dist (f₁.toFun t) (f₂.toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
t : ↑(Icc v.tMin v.tMax)
⊢ dist (f₁.next.toFun t) (f₂.next.toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d

Tactic:
simp only [dist_eq_norm, next_apply, add_sub_add_left_eq_sub, ←
  intervalIntegral.integral_sub (intervalIntegrable_vComp _ _ _)
    (intervalIntegrable_vComp _ _ _),
  norm_integral_eq_norm_integral_Ioc] at *

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (x : ℝ) in Ι ↑v.t₀ ↑t, f₁.vComp x - f₂.vComp x ∂volume‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (↑v.t₀ ⊓ ↑t) (↑v.t₀ ⊔ ↑t)
⊢ τ ∈ Icc v.tMin v.tMax

Tactic:
exact uIcc_subset_Icc v.t₀.2 t.2 <| Ioc_subset_Icc_self hτ

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ Continuous fun τ => ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)

Tactic:
fun_prop

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, f₁.vComp τ - f₂.vComp τ‖ ≤
    ∫ (τ : ℝ) in Ι ↑v.t₀ ↑t, ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)

Tactic:
refine norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop)) ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ι ↑v.t₀ ↑t), ‖f₁.vComp x - f₂.vComp x‖ ≤ ↑v.L * ((↑v.L * |x - ↑v.t₀|) ^ n / ↑n ! * d)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ‖∫ (x : ℝ) in Ι ↑v.t₀ ↑t, f₁.vComp x - f₂.vComp x ∂volume‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d

Tactic:
calc
  ‖∫ τ in Ι (v.t₀ : ℝ) t, f₁.vComp τ - f₂.vComp τ‖ ≤
      ∫ τ in Ι (v.t₀ : ℝ) t, v.L * ((v.L * |τ - v.t₀|) ^ n / n ! * d) := by
    refine norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop)) ?_
    refine (ae_restrict_mem measurableSet_Ioc).mono fun τ hτ ↦ ?_
    refine (v.lipschitzOnWith (v.proj τ).2).norm_sub_le_of_le (f₁.mem_closedBall _)
        (f₂.mem_closedBall _) ((h _).trans_eq ?_)
    rw [v.proj_of_mem]
    exact uIcc_subset_Icc v.t₀.2 t.2 <| Ioc_subset_Icc_self hτ
  _ = (v.L * |t.1 - v.t₀|) ^ (n + 1) / (n + 1)! * d := by
    simp_rw [mul_pow, div_eq_mul_inv, mul_assoc, MeasureTheory.integral_mul_left,
      MeasureTheory.integral_mul_right, integral_pow_abs_sub_uIoc, div_eq_mul_inv,
      pow_succ' (v.L : ℝ), Nat.factorial_succ, Nat.cast_mul, Nat.cast_succ, mul_inv, mul_assoc]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ι ↑v.t₀ ↑t), ‖f₁.vComp x - f₂.vComp x‖ ≤ ↑v.L * ((↑v.L * |x - ↑v.t₀|) ^ n / ↑n ! * d)

Tactic:
refine (ae_restrict_mem measurableSet_Ioc).mono fun τ hτ ↦ ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
d : ℝ
t : ↑(Icc v.tMin v.tMax)
h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d
τ : ℝ
hτ : τ ∈ Ioc (↑v.t₀ ⊓ ↑t) (↑v.t₀ ⊔ ↑t)
⊢ ‖f₁.vComp τ - f₂.vComp τ‖ ≤ ↑v.L * ((↑v.L * |τ - ↑v.t₀|) ^ n / ↑n ! * d)