internlm/Lean-Github huggingface dataset:
Theorem: hasDerivAt_e
Proof state before:
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ HasDerivAt (⇑(e u)) (-2 * ↑π * ↑u * I * (e u) x) x
Tactic:
convert (hasDerivAt_fourierChar (-x * u)).scomp x l2 using 1
Proof state after:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ -2 * ↑π * ↑u * I * (e u) x = -u • (2 * ↑π * I * ↑(𝐞 (-x * u)))
Theorem: hasDerivAt_e
Proof state before:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ -2 * ↑π * ↑u * I * (e u) x = -u • (2 * ↑π * I * ↑(𝐞 (-x * u)))
Tactic:
simp
Proof state after:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ 2 * ↑π * ↑u * I * ↑(𝐞 (-(x * u))) = ↑u * (2 * ↑π * I * ↑(𝐞 (-(x * u))))
Theorem: hasDerivAt_e
Proof state before:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ 2 * ↑π * ↑u * I * ↑(𝐞 (-(x * u))) = ↑u * (2 * ↑π * I * ↑(𝐞 (-(x * u))))
Tactic:
ring
Proof state after:
no goals
Theorem: hasDerivAt_e
Proof state before:
u x : ℝ
⊢ HasDerivAt (fun v => -v * u) (-u) x
Tactic:
simpa only [neg_mul_comm] using hasDerivAt_mul_const (-u)
Proof state after:
no goals
Theorem: F_neg
Proof state before:
f : ℝ → ℂ
u : ℝ
⊢ 𝓕 (fun x => -f x) u = -𝓕 f u
Tactic:
simp [fourierIntegral_eq, integral_neg]
Proof state after:
no goals
Theorem: F_add
Proof state before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Continuous fun p => ((innerₗ ℝ) p.1) p.2
Tactic:
exact continuous_mul
Proof state after:
no goals
Theorem: F_sub
Proof state before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x - g x) x = 𝓕 f x - 𝓕 g x
Tactic:
simp_rw [sub_eq_add_neg]
Proof state after:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x + -g x) x = 𝓕 f x + -𝓕 g x
Theorem: F_sub
Proof state before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x + -g x) x = 𝓕 f x + -𝓕 g x
Tactic:
rw [F_add]
Proof state after:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x) x + 𝓕 (fun x => -g x) x = 𝓕 f x + -𝓕 g x

case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Theorem: F_sub
Proof state before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x) x + 𝓕 (fun x => -g x) x = 𝓕 f x + -𝓕 g x

case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Tactic:
simp
Proof state after:
case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Theorem: F_sub
Proof state before:
case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Tactic:
exact hf
Proof state after:
case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Theorem: F_sub
Proof state before:
case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Tactic:
exact hg.neg
Proof state after:
no goals
Theorem: F_mul
Proof state before:
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ 𝓕 (fun x => c * f x) u = c * 𝓕 f u
Tactic:
simp [fourierIntegral_real_eq, ← integral_mul_left]
Proof state after:
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ ∫ (v : ℝ), 𝐞 (-(v * u)) • (c * f v) = ∫ (a : ℝ), c * 𝐞 (-(a * u)) • f a
Theorem: F_mul
Proof state before:
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ ∫ (v : ℝ), 𝐞 (-(v * u)) • (c * f v) = ∫ (a : ℝ), c * 𝐞 (-(a * u)) • f a
Tactic:
congr
Proof state after:
case e_f
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ (fun v => 𝐞 (-(v * u)) • (c * f v)) = fun a => c * 𝐞 (-(a * u)) • f a
Theorem: F_mul
Proof state before:
case e_f
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ (fun v => 𝐞 (-(v * u)) • (c * f v)) = fun a => c * 𝐞 (-(a * u)) • f a
Tactic:
ext
Proof state after:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ 𝐞 (-(x✝ * u)) • (c * f x✝) = c * 𝐞 (-(x✝ * u)) • f x✝
Theorem: F_mul
Proof state before:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ 𝐞 (-(x✝ * u)) • (c * f x✝) = c * 𝐞 (-(x✝ * u)) • f x✝
Tactic:
simp [Real.fourierChar, expMapCircle]
Proof state after:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * (c * f x✝) = c * (cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * f x✝)
Theorem: F_mul
Proof state before:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * (c * f x✝) = c * (cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * f x✝)
Tactic:
ring
Proof state after:
no goals
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
have l1 : Integrable (fun x => (((π : ℂ) ^ 2)⁻¹ * 4⁻¹) * deriv (deriv f) x) := by
  apply Integrable.const_mul ; simpa [iteratedDeriv_succ] using f.integrable le_rfl
Proof state after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
have l4 : Differentiable ℝ f := f.differentiable
Proof state after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
have l5 : Differentiable ℝ (deriv f) := f.deriv.differentiable
Proof state after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (1 + ↑u ^ 2) * 𝓕 f.toFun u = 𝓕 (fun u => f.toFun u - 1 / (4 * ↑π ^ 2) * deriv^[2] f.toFun u) u
Tactic:
simp [f.hf, l1, add_mul, Real.fourierIntegral_deriv f.hf' l5 f.hf'', Real.fourierIntegral_deriv f.hf l4 f.hf']
Proof state after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u =
    𝓕 (fun x => f.toFun x) u - (↑π ^ 2)⁻¹ * 4⁻¹ * (2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u))
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u =
    𝓕 (fun x => f.toFun x) u - (↑π ^ 2)⁻¹ * 4⁻¹ * (2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u))
Tactic:
field_simp [pi_ne_zero]
Proof state after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u) * (↑π ^ 2 * 4) =
    𝓕 (fun x => f.toFun x) u * (↑π ^ 2 * 4) - 2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u)
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ (𝓕 f.toFun u + ↑u ^ 2 * 𝓕 f.toFun u) * (↑π ^ 2 * 4) =
    𝓕 (fun x => f.toFun x) u * (↑π ^ 2 * 4) - 2 * ↑π * I * ↑u * (2 * ↑π * I * ↑u * 𝓕 f.toFun u)
Tactic:
ring_nf
Proof state after:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * 4 + 𝓕 f.toFun u * ↑π ^ 2 * 4 =
    -(𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * I ^ 2 * 4) + 𝓕 (fun x => f.toFun x) u * ↑π ^ 2 * 4
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
l1 : Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
l4 : Differentiable ℝ f.toFun
l5 : Differentiable ℝ (deriv f.toFun)
⊢ 𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * 4 + 𝓕 f.toFun u * ↑π ^ 2 * 4 =
    -(𝓕 f.toFun u * ↑u ^ 2 * ↑π ^ 2 * I ^ 2 * 4) + 𝓕 (fun x => f.toFun x) u * ↑π ^ 2 * 4
Tactic:
simp
Proof state after:
no goals
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
f : W21
u : ℝ
⊢ Integrable (fun x => (↑π ^ 2)⁻¹ * 4⁻¹ * deriv (deriv f.toFun) x) volume
Tactic:
apply Integrable.const_mul
Proof state after:
case h
f : W21
u : ℝ
⊢ Integrable (fun x => deriv (deriv f.toFun) x) volume
Theorem: fourierIntegral_self_add_deriv_deriv
Proof state before:
case h
f : W21
u : ℝ
⊢ Integrable (fun x => deriv (deriv f.toFun) x) volume
Tactic:
simpa [iteratedDeriv_succ] using f.integrable le_rfl
Proof state after:
no goals
Theorem: deriv_ofReal
Proof state before:
⊢ deriv ofReal' = fun x => 1
Tactic:
ext x
Proof state after:
case h
x : ℝ
⊢ deriv ofReal' x = 1
Theorem: deriv_ofReal
Proof state before:
case h
x : ℝ
⊢ deriv ofReal' x = 1
Tactic:
exact ((hasDerivAt_id x).ofReal_comp).deriv
Proof state after:
no goals
Theorem: Asymptotics.isTheta_bot
Proof state before:
α : Type u_1
β : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_5
inst✝² : Norm E
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =Θ[⊥] g
Tactic:
simp [IsTheta]
Proof state after:
no goals
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto f p (𝓝 ℓ)
Tactic:
rw [tendsto_nhds_left]
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p (𝓤 β)
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
⊢ Tendsto (fun x => (f x, ℓ)) p (𝓤 β)
Tactic:
intro s hs
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ s ∈ map (fun x => (f x, ℓ)) p
Tactic:
change ∀ᶠ x in p, (f x, ℓ) ∈ s
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
obtain ⟨t, ht, hts⟩ := comp3_mem_uniformity hs
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
have l1 : ∀ᶠ i in l, (L i, ℓ) ∈ t := tendsto_nhds_left.mp h3 ht
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
have l2 : ∀ᶠ i in l, ∀ᶠ x in p, (F i x, L i) ∈ t := by
  filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
have l3 : ∀ᶠ i in l, ∀ᶠ x in p, (f x, F i x) ∈ t := (h1 t ht).curry
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
obtain ⟨i, l4, l5, l6⟩ := (l1.and (l2.and l3)).exists
Proof state after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
i : ι
l4 : (L i, ℓ) ∈ t
l5 : ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l6 : ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
l2 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l3 : ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
i : ι
l4 : (L i, ℓ) ∈ t
l5 : ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
l6 : ∀ᶠ (x : α) in p, (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p, (f x, ℓ) ∈ s
Tactic:
filter_upwards [l5, l6] with x l5 l6 using hts ⟨F i x, l6, L i, l5, l4⟩
Proof state after:
no goals
Theorem: TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
p : Filter α
b : β
F : ι → α → β
f : α → β
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f l p
h2 : ∀ᶠ (i : ι) in l, Tendsto (F i) p (𝓝 (L i))
h3 : Tendsto L l (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : t ○ (t ○ t) ⊆ s
l1 : ∀ᶠ (i : ι) in l, (L i, ℓ) ∈ t
⊢ ∀ᶠ (i : ι) in l, ∀ᶠ (x : α) in p, (F i x, L i) ∈ t
Tactic:
filter_upwards [h2] with i h2 using tendsto_nhds_left.mp h2 ht
Proof state after:
no goals
Theorem: integrable_iff_integrableAtFilter_atBot_atTop
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
Tactic:
use fun hf ↦ ⟨⟨hf.integrableAtFilter _, hf.integrableAtFilter _⟩, hf.locallyIntegrable⟩
Proof state after:
case mpr
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ
Theorem: integrable_iff_integrableAtFilter_atBot_atTop
Proof state before:
case mpr
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ
Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
Proof state after:
case mpr
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Theorem: integrable_iff_integrableAtFilter_atBot_atTop
Proof state before:
case mpr
X : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Tactic:
exact (IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop
Proof state after:
no goals
Theorem: integrable_iff_integrableAtFilter_atBot
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
Tactic:
use fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩
Proof state after:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ
Theorem: integrable_iff_integrableAtFilter_atBot
Proof state before:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ → Integrable f μ
Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
Proof state after:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Theorem: integrable_iff_integrableAtFilter_atBot
Proof state before:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Tactic:
exact h.1.filter_mono cocompact_le_atBot
Proof state after:
no goals
Theorem: integrable_iff_integrableAtFilter_atTop
Proof state before:
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ
Tactic:
use fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩
Proof state after:
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ → Integrable f μ