# Zulip Chat Archive

## 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 _ _ _,
add_mem' := λ f g hf hg, integrable.add hf hg,
smul_mem' := λ c f hf, integrable.smul c hf },
let φp0 : p →ₗ[ℝ] ℝ :=
{ to_fun := λ f, ∫ x, f x ∂μ,
map_add' := λ f g, integral_add f.2 g.2,
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?

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

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,
add_mem' := sorry,
smul_mem' := sorry },
let φp0 : p →ₗ[ℝ] ℝ :=
{ to_fun := λ f, ∫ x, f x ∂μ,
map_add' := sorry,
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 _ _ _,
add_mem' := λ f g hf hg, integrable.add hf hg,
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_add' := λ f g, integral_add f.2 g.2,
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