## Stream: general

### Topic: kernel stuck at checking a definition

#### Sebastien Gouezel (May 08 2021 at 12:35):

I have a very weird behavior where everything seems to go right, but at the end of a definition the kernel seems to be stuck forever.

import analysis.normed_space.hahn_banach
import topology.continuous_function.bounded
import measure_theory.bochner_integration

universe u
variable {α : Type u}

open measure_theory set
open_locale bounded_continuous_function
noncomputable theory

instance [topological_space α] : semi_normed_group (α →ᵇ ℝ) := normed_group.to_semi_normed_group

/-- Given a measure, there exists a continuous linear form on the space of all bounded functions
(not necessarily measurable) that coincides with the integral on bounded measurable functions. -/
lemma measure.linear_extension_to_bounded_functions [topological_space α]
[measurable_space α] {μ : measure α} [finite_measure μ] :
true :=
begin
let p : subspace ℝ (α →ᵇ ℝ) :=
{ carrier := {f | integrable f μ},
zero_mem' := integrable_zero _ _ _,
smul_mem' := λ c f hf, integrable.smul c hf },
let φp0 : p →ₗ[ℝ] ℝ :=
{ to_fun := λ f, ∫ x, f x ∂μ,
map_smul' := λ c f, integral_smul _ _ },
let φp : p →L[ℝ] ℝ :=
begin
have n : ℕ, -- this line and the next line are here just to make sure that there is
swap,          -- a goal left after solving the main goal
apply linear_map.mk_continuous φp0 (μ univ).to_real _,
rintros ⟨f, hf⟩,
rw mul_comm,
apply norm_integral_le_of_norm_le_const,
apply filter.eventually_of_forall,
assume x,
exact bounded_continuous_function.norm_coe_le_norm f x,
-- the main goal is solved, but if you solve the side goal with
-- exact 1,
-- then the kernel is stuck forever
end,
trivial,
end


#### Eric Wieser (May 08 2021 at 12:36):

Does closing the side goal with sorry also leave the kernel stuck?

Yes

#### Patrick Massot (May 08 2021 at 12:43):

Since you seem to be in a measure theoretic mood, would you mind having a look at #7437?

#### Eric Wieser (May 08 2021 at 12:44):

Does replacing the exact bounded_... with sorry also stick the kernel?

#### Kevin Buzzard (May 08 2021 at 12:52):

import analysis.normed_space.hahn_banach
import topology.continuous_function.bounded
import measure_theory.bochner_integration

universe u
variable {α : Type u}

open measure_theory set
open_locale bounded_continuous_function
noncomputable theory

instance [topological_space α] : semi_normed_group (α →ᵇ ℝ) := normed_group.to_semi_normed_group

lemma measure.linear_extension_to_bounded_functions [topological_space α]
[measurable_space α] {μ : measure α} [finite_measure μ] :
true :=
begin
let p : subspace ℝ (α →ᵇ ℝ) :=
{ carrier := {f | integrable f μ},
zero_mem' := sorry,
smul_mem' := sorry },
let φp0 : p →ₗ[ℝ] ℝ :=
{ to_fun := λ f, ∫ x, f x ∂μ,
map_smul' := sorry },
let φp : p →L[ℝ] ℝ := linear_map.mk_continuous φp0 (μ univ).to_real sorry,
trivial,
end


also gets stuck (and eventually results in a deterministic timeout)

#### Kevin Buzzard (May 08 2021 at 12:53):

If you set_option trace.class_instances true you can see stuff going crazy

#### Eric Wieser (May 08 2021 at 12:57):

It's easy to get waylaid here by the fact the kernel doesn't complain until you actually close all the goals (even with sorry)

#### Kevin Buzzard (May 08 2021 at 13:05):

Oh I don't think the issue is trace.class_instances.

import analysis.normed_space.hahn_banach
import topology.continuous_function.bounded
import measure_theory.bochner_integration

universe u
variable {α : Type u}

open measure_theory set
open_locale bounded_continuous_function
noncomputable theory

instance [topological_space α] : semi_normed_group (α →ᵇ ℝ) := normed_group.to_semi_normed_group

-- succeeds in a second or two
example [topological_space α] [measurable_space α] {μ : measure α} [finite_measure μ] : (⊥ : subspace ℝ (α →ᵇ ℝ)) →L[ℝ] ℝ :=
linear_map.mk_continuous (0 : (⊥ : subspace ℝ (α →ᵇ ℝ)) →ₗ[ℝ] ℝ) (μ univ).to_real sorry

-- loops
lemma measure.linear_extension_to_bounded_functions [topological_space α]
[measurable_space α] {μ : measure α} [finite_measure μ] :
true :=
begin
let φp : (⊥ : subspace ℝ (α →ᵇ ℝ)) →L[ℝ] ℝ := linear_map.mk_continuous (0 : (⊥ : subspace ℝ (α →ᵇ ℝ)) →ₗ[ℝ] ℝ) (μ univ).to_real sorry,
trivial,
end


#### Kevin Buzzard (May 08 2021 at 13:08):

-- works
def foo [topological_space α] [measurable_space α] (μ : measure α) [finite_measure μ] : (⊥ : subspace ℝ (α →ᵇ ℝ)) →L[ℝ] ℝ :=
linear_map.mk_continuous (0 : (⊥ : subspace ℝ (α →ᵇ ℝ)) →ₗ[ℝ] ℝ) (μ univ).to_real sorry

-- also works
lemma measure.linear_extension_to_bounded_functions [topological_space α]
[measurable_space α] {μ : measure α} [finite_measure μ] :
true :=
begin
let φp : (⊥ : subspace ℝ (α →ᵇ ℝ)) →L[ℝ] ℝ := foo μ,
trivial,
end


So there's a potential workaround

#### Kevin Buzzard (May 08 2021 at 13:15):

Problem magically goes away if you pull out all the auxiliary defs:

import analysis.normed_space.hahn_banach
import topology.continuous_function.bounded
import measure_theory.bochner_integration

universe u
variable {α : Type u}

open measure_theory set
open_locale bounded_continuous_function
noncomputable theory

instance [topological_space α] : semi_normed_group (α →ᵇ ℝ) := normed_group.to_semi_normed_group

def foo_p [topological_space α] [measurable_space α] (μ : measure α) [finite_measure μ] : subspace ℝ (α →ᵇ ℝ) :=
{ carrier := {f | integrable f μ},
zero_mem' := integrable_zero _ _ _,
smul_mem' := λ c f hf, integrable.smul c hf }

def foo_φp0 [topological_space α] [measurable_space α] (μ : measure α) [finite_measure μ] :
foo_p μ →ₗ[ℝ] ℝ :=
{ to_fun := λ f, ∫ x, f x ∂μ,
map_smul' := λ c f, integral_smul _ _ }

def foo_φp [topological_space α] [measurable_space α] (μ : measure α) [finite_measure μ] : foo_p μ →L[ℝ] ℝ :=
begin
apply linear_map.mk_continuous (foo_φp0 μ) (μ univ).to_real _,
rintros ⟨f, hf⟩,
rw mul_comm,
apply norm_integral_le_of_norm_le_const,
apply filter.eventually_of_forall,
assume x,
exact bounded_continuous_function.norm_coe_le_norm f x,
end

/-- Given a measure, there exists a continuous linear form on the space of all bounded functions
(not necessarily measurable) that coincides with the integral on bounded measurable functions. -/
lemma measure.linear_extension_to_bounded_functions [topological_space α]
[measurable_space α] {μ : measure α} [finite_measure μ] :
true :=
begin
have n : ℕ, swap,
let p : subspace ℝ (α →ᵇ ℝ) := foo_p μ,
let φp0 : p →ₗ[ℝ] ℝ := foo_φp0 μ,
let φp : p →L[ℝ] ℝ := foo_φp μ,
trivial,
exact 1,
end


#### Sebastien Gouezel (May 08 2021 at 15:08):

Kevin Buzzard said:

Problem magically goes away if you pull out all the auxiliary defs:

Thanks a lot for investigating this. Indeed, this solves my issue completely. I'd like to understand better what is going on, but I'll take the message that defining complicated objects inside proofs is broken, and that they should be defined separately.

#### Kevin Buzzard (May 08 2021 at 15:57):

Yes I am also completely bewildered about why your code hangs Lean, this we didn't solve at all.

Last updated: Aug 03 2023 at 10:10 UTC