internlm/Lean-Github huggingface dataset:
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
Tactic:
have : μ = Measure.map L.symm ν := by
  simp [Measure.map_map L.symm.continuous.measurable L.continuous.measurable]
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
this : μ = map (⇑L.symm) ν
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
this : μ = map (⇑L.symm) ν
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
Tactic:
have hL : ClosedEmbedding L.symm := L.symm.toHomeomorph.closedEmbedding
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL✝ : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
this : μ = map (⇑L.symm) ν
hL : ClosedEmbedding ⇑L.symm
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL✝ : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
this : μ = map (⇑L.symm) ν
hL : ClosedEmbedding ⇑L.symm
⊢ ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
Tactic:
simpa [this, hL.integral_map] using H
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
⊢ μ = map (⇑L.symm) ν
Tactic:
simp [Measure.map_map L.symm.continuous.measurable L.continuous.measurable]
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hf'g
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
⊢ Integrable (fun x => (B (f' (L.symm x))) (g (L.symm x))) ν
Tactic:
simpa [L_emb.integrable_map_iff, Function.comp] using hf'g
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hfg'
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
⊢ Integrable (fun x => (B (f (L.symm x))) (g' (L.symm x))) ν
Tactic:
simpa [L_emb.integrable_map_iff, Function.comp] using hfg'
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hfg
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
⊢ Integrable (fun x => (B (f (L.symm x))) (g (L.symm x))) ν
Tactic:
simpa [L_emb.integrable_map_iff, Function.comp] using hfg
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
⊢ ∀ (x : E' × ℝ), HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Tactic:
intro x
Proof state after:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Tactic:
have : f = (f ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp
Proof state after:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Tactic:
specialize hf (L.symm x)
Proof state after:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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)) μ
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
hf : HasLineDerivAt ℝ f (f' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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)) μ
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
hf : HasLineDerivAt ℝ f (f' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Tactic:
rw [this] at hf
Proof state after:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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)) μ
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
hf : HasLineDerivAt ℝ ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) (f' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hf
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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)) μ
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
hf : HasLineDerivAt ℝ ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) (f' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => f (L.symm x)) (f' (L.symm x)) x (0, 1)
Tactic:
convert hf.of_comp using 1
Proof state after:
case h.e'_11
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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)) μ
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
hf : HasLineDerivAt ℝ ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) (f' (L.symm x)) (L.symm x) v
⊢ x = ↑↑L (L.symm x)

case h.e'_12
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
inst✝ : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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)) μ
hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this✝ : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : L v = (0, 1)
ν : Measure (E' × ℝ) := map (⇑L) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
this : f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
hf : HasLineDerivAt ℝ ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) (f' (L.symm x)) (L.symm x) v
⊢ (0, 1) = ↑↑L v