internlm/Lean-Github huggingface dataset:
Theorem: intervalIntegral.integral_deriv_bilin_eq_sub
Proof 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'
Proof state after:
no goals
Theorem: intervalIntegral.integral_deriv_bilin_eq_sub
Proof 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)
Proof state after:
no goals
Theorem: intervalIntegral.integral_deriv_bilin_eq_sub
Proof 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'
Proof state after:
no goals
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof 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 b)) (v b) - (B (u a)) (v a) - ∫ (x : ℝ) in a..b, (B (u' x)) (v x)
Tactic:
rw [← integral_deriv_bilin_eq_sub B hu hv hu' hv']
Proof 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)
⊢ ∫ (x : ℝ) in a..b, (B (u x)) (v' x) =
    (∫ (x : ℝ) in a..b, (B (u' x)) (v x) + (B (u x)) (v' x)) - ∫ (x : ℝ) in a..b, (B (u' x)) (v x)
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hf
𝕜 : 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

case hg
𝕜 : 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)) volume a b
Tactic:
. refine (ContinuousOn.add ?_ ?_).intervalIntegrable
  . exact ContinuousOn.bilin hu' (HasDerivAt.continuousOn hv)
  . exact ContinuousOn.bilin (HasDerivAt.continuousOn hu) hv'
Proof state after:
case hg
𝕜 : 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)) volume a b
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof 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) = ∫ (x : ℝ) in a..b, (B (u' x)) (v x) + (B (u x)) (v' x) - (B (u' x)) (v x)
Tactic:
simp
Proof state after:
no goals
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hf
𝕜 : 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
Proof state after:
case hf.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 hf.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)
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hf.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 hf.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)
Proof state after:
case hf.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)
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hf.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'
Proof state after:
no goals
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hf.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)
Proof state after:
no goals
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hf.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'
Proof state after:
no goals
Theorem: intervalIntegral.integral_bilin_deriv_eq_deriv_bilin
Proof state before:
case hg
𝕜 : 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)) volume a b
Tactic:
exact (ContinuousOn.bilin hu' (HasDerivAt.continuousOn hv)).intervalIntegrable
Proof state after:
no goals
Theorem: norm_innerSL_le_one
Proof state before:
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ‖innerSL 𝕜‖ ≤ 1
Tactic:
simp [ContinuousLinearMap.opNorm_le_iff]
Proof state after:
no goals
Theorem: Function.update_mul_update
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝¹ : (i : α) → Monoid (β i)
inst✝ : DecidableEq α
a : α
f : (a : α) → β a
b : β a
⊢ (update f a 1 * update (fun x => 1) a b) a = b
Tactic:
simp
Proof state after:
no goals
Theorem: Function.update_mul_update
Proof state before:
α : Type u_1
β : α → Type u_2
inst✝¹ : (i : α) → Monoid (β i)
inst✝ : DecidableEq α
a : α
f : (a : α) → β a
b : β a
i : α
h : i ≠ a
⊢ (update f a 1 * update (fun x => 1) a b) i = f i
Tactic:
simp [h]
Proof state after:
no goals
Theorem: iteratedDeriv_pow
Proof state before:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
⊢ (iteratedDeriv Nat.zero fun x => x ^ n) = fun x => ↑(Nat.descFactorial n Nat.zero) * x ^ (n - Nat.zero)
Tactic:
simp
Proof state after:
no goals
Theorem: iteratedDeriv_pow
Proof state before:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
⊢ (iteratedDeriv (Nat.succ i) fun x => x ^ n) = fun x => ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
rw [iteratedDeriv_succ, IH]
Proof state after:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
⊢ (deriv fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) = fun x =>
    ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Theorem: iteratedDeriv_pow
Proof state before:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
⊢ (deriv fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) = fun x =>
    ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
funext x
Proof state after:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ deriv (fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Theorem: iteratedDeriv_pow
Proof state before:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ deriv (fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
rw [deriv_const_mul _ (differentiableAt_pow (n - i)), deriv_pow]
Proof state after:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * (↑(n - i) * x ^ (n - i - 1)) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Theorem: iteratedDeriv_pow
Proof state before:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * (↑(n - i) * x ^ (n - i - 1)) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
rw [← mul_assoc]
Proof state after:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) * x ^ (n - i - 1) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Theorem: iteratedDeriv_pow
Proof state before:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) * x ^ (n - i - 1) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
refine congrArg₂ _ ?_ ?_
Proof state after:
case succ.h.refine_1
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) = ↑(Nat.descFactorial n (Nat.succ i))

case succ.h.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ x ^ (n - i - 1) = x ^ (n - Nat.succ i)
Theorem: iteratedDeriv_pow
Proof state before:
case succ.h.refine_1
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) = ↑(Nat.descFactorial n (Nat.succ i))
Tactic:
simp [mul_comm (↑(n - i) : 𝕜)]
Proof state after:
no goals