Theorem: intervalIntegral.integral_deriv_bilin_eq_sub (ForML/Util.lean)

State before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ∫ (x : ℝ) in a..b, (B (u' x)) (v x) + (B (u x)) (v' x) = (B (u b)) (v b) - (B (u a)) (v a)
Tactic:
refine integral_eq_sub_of_hasDerivAt (fun x hx => HasDerivAt.bilin B (hu x hx) (hv x hx)) ?_
State after:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ IntervalIntegrable (fun x => (B (u' x)) (v x) + (B (u x)) (v' x)) volume a b

State before:
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ IntervalIntegrable (fun x => (B (u' x)) (v x) + (B (u x)) (v' x)) volume a b
Tactic:
refine (ContinuousOn.add ?_ ?_).intervalIntegrable
State after:
case refine_1
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u' x)) (v x)) (Set.uIcc a b)

case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)

State before:
case refine_1
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u' x)) (v x)) (Set.uIcc a b)

case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)
Tactic:
. exact ContinuousOn.bilin hu' (HasDerivAt.continuousOn hv)
State after:
case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)

State before:
case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)
Tactic:
. exact ContinuousOn.bilin (HasDerivAt.continuousOn hu) hv'
State after:
no goals

State before:
case refine_1
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u' x)) (v x)) (Set.uIcc a b)
Tactic:
exact ContinuousOn.bilin hu' (HasDerivAt.continuousOn hv)
State after:
no goals

State before:
case refine_2
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
a b : ℝ
u u' : ℝ → E
v v' : ℝ → F
B : E →L[ℝ] F →L[ℝ] G
hu : ∀ x ∈ Set.uIcc a b, HasDerivAt u (u' x) x
hv : ∀ x ∈ Set.uIcc a b, HasDerivAt v (v' x) x
hu' : ContinuousOn u' (Set.uIcc a b)
hv' : ContinuousOn v' (Set.uIcc a b)
⊢ ContinuousOn (fun x => (B (u x)) (v' x)) (Set.uIcc a b)
Tactic:
exact ContinuousOn.bilin (HasDerivAt.continuousOn hu) hv'
State after:
no goals