internlm/Lean-Github huggingface dataset:
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
case h
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
⊢ ∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) = -∫ (t : ℝ), (B (f' (x, t))) (g (x, t))
Tactic:
apply integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable ?_ ?_ hfg'x hf'gx hfgx
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
⊢ ∀ (x_1 : ℝ), HasDerivAt (fun x_2 => f (x, x_2)) (f' (x, x_1)) x_1

E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
⊢ ∀ (x_1 : ℝ), HasDerivAt (fun x_2 => g (x, x_2)) (g' (x, x_1)) x_1
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
⊢ ∀ (x_1 : ℝ), HasDerivAt (fun x_2 => f (x, x_2)) (f' (x, x_1)) x_1
Tactic:
intro t
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ HasDerivAt (fun x_1 => f (x, x_1)) (f' (x, t)) t
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ HasDerivAt (fun x_1 => f (x, x_1)) (f' (x, t)) t
Tactic:
convert (hf (x, t)).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t))) (by simp)
  <;> simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ 0 = id t + -t
Tactic:
simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
⊢ ∀ (x_1 : ℝ), HasDerivAt (fun x_2 => g (x, x_2)) (g' (x, x_1)) x_1
Tactic:
intro t
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ HasDerivAt (fun x_1 => g (x, x_1)) (g' (x, t)) t
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
x : E
hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume
hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume
hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume
t : ℝ
⊢ HasDerivAt (fun x_1 => g (x, x_1)) (g' (x, t)) t
Tactic:
convert (hg (x, t)).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t))) (by simp)
  <;> simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace ℝ G
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)
hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)
hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
⊢ ∫ (x : E), -∫ (t : ℝ), (B (f' (x, t))) (g (x, t)) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.prod volume
Tactic:
rw [integral_neg, integral_prod _ hf'g]
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Tactic:
let ν : Measure E := addHaar
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Tactic:
have A : ν.prod volume = (addHaarScalarFactor (ν.prod volume) μ) • μ :=
  isAddLeftInvariant_eq_smul _ _
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Tactic:
have Hf'g : Integrable (fun x ↦ B (f' x) (g x)) (ν.prod volume) := by
  rw [A]; exact hf'g.smul_measure_nnreal
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Tactic:
have Hfg' : Integrable (fun x ↦ B (f x) (g' x)) (ν.prod volume) := by
  rw [A]; exact hfg'.smul_measure_nnreal
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Tactic:
have Hfg : Integrable (fun x ↦ B (f x) (g x)) (ν.prod volume) := by
  rw [A]; exact hfg.smul_measure_nnreal
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)
Hfg : Integrable (fun x => (B (f x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)
Hfg : Integrable (fun x => (B (f x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ
Tactic:
rw [isAddLeftInvariant_eq_smul μ (ν.prod volume)]
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ✝ : Measure E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst✝ : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g : Integrable (fun x => (B (f' x)) (g x)) μ
hfg' : Integrable (fun x => (B (f x)) (g' x)) μ
hfg : Integrable (fun x => (B (f x)) (g x)) μ
hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ
Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)
Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)
Hfg : Integrable (fun x => (B (f x)) (g x)) (ν.prod volume)
⊢ ∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ.addHaarScalarFactor (ν.prod volume) • ν.prod volume =
    -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.addHaarScalarFactor (ν.prod volume) • ν.prod volume