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) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
⊢ f = (f ∘ ⇑L.symm) ∘ ⇑↑↑L
Tactic:
ext y
Proof state after:
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✝¹ : 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' × ℝ
y : E
⊢ f y = ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) y
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
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✝¹ : 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' × ℝ
y : E
⊢ f y = ((f ∘ ⇑L.symm) ∘ ⇑↑↑L) y
Tactic:
simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
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)
Tactic:
simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
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
Tactic:
simp [← hL]
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hg
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 => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Tactic:
intro x
Proof state after:
case pos.inr.intro.hg
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 => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hg
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 => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Tactic:
have : g = (g ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp
Proof state after:
case pos.inr.intro.hg
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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
⊢ HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hg
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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
⊢ HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Tactic:
specialize hg (L.symm x)
Proof state after:
case pos.inr.intro.hg
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
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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ g (g' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hg
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
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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ g (g' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Tactic:
rw [this] at hg
Proof state after:
case pos.inr.intro.hg
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
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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
case pos.inr.intro.hg
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
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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (L.symm x)) (L.symm x) v
⊢ HasLineDerivAt ℝ (fun x => g (L.symm x)) (g' (L.symm x)) x (0, 1)
Tactic:
convert hg.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)) μ
hf : ∀ (x : E), HasLineDerivAt ℝ f (f' 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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (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)) μ
hf : ∀ (x : E), HasLineDerivAt ℝ f (f' 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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (L.symm x)) (L.symm x) v
⊢ (0, 1) = ↑↑L v
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) μ
L_emb : MeasurableEmbedding ⇑L
x : E' × ℝ
⊢ g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
Tactic:
ext y
Proof state after:
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✝¹ : 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' × ℝ
y : E
⊢ g y = ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) y
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
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✝¹ : 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' × ℝ
y : E
⊢ g y = ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) y
Tactic:
simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
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)) μ
hf : ∀ (x : E), HasLineDerivAt ℝ f (f' 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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (L.symm x)) (L.symm x) v
⊢ x = ↑↑L (L.symm x)
Tactic:
simp
Proof state after:
no goals
Theorem: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable
Proof state before:
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)) μ
hf : ∀ (x : E), HasLineDerivAt ℝ f (f' 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 : g = (g ∘ ⇑L.symm) ∘ ⇑↑↑L
hg : HasLineDerivAt ℝ ((g ∘ ⇑L.symm) ∘ ⇑↑↑L) (g' (L.symm x)) (L.symm x) v
⊢ (0, 1) = ↑↑L v
Tactic:
simp [← hL]
Proof state after:
no goals
Theorem: BrunTitchmarsh.siftedSum_eq_card
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).siftedSum =
    ↑(Finset.filter (fun d => ∀ (p : ℕ), p.Prime → ↑p ≤ z → ¬p ∣ d) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card
Tactic:
apply Sieve.siftedSum_eq
Proof state after:
case hw
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ i ∈ (primeInterSieve x y z hz).support, (primeInterSieve x y z hz).weights i = 1

case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Theorem: BrunTitchmarsh.siftedSum_eq_card
Proof state before:
case hw
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ i ∈ (primeInterSieve x y z hz).support, (primeInterSieve x y z hz).weights i = 1

case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Tactic:
exact fun _ _ => rfl
Proof state after:
case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Theorem: BrunTitchmarsh.siftedSum_eq_card
Proof state before:
case hz
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ 1 ≤ z

case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Tactic:
exact hz
Proof state after:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Theorem: BrunTitchmarsh.siftedSum_eq_card
Proof state before:
case hP
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (primeInterSieve x y z hz).prodPrimes = primorial ⌊z⌋₊
Tactic:
rfl
Proof state after:
no goals