kernel stuck at checking a definition

Stream: general

[Sebastien Gouezel]

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]

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

[Sebastien Gouezel]

Yes

[Patrick Massot]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

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]

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]

-- 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]

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]

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]

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