Zulip Chat Archive

Stream: general

Topic: complete_space by cases


Rémy Degenne (Feb 10 2021 at 17:19):

On branch#Lp_complete , I am working on a proof of completeness of Lp spaces. I did it separately for two cases (p infinite, or not). Now I want to put those together into one final theorem . However I encounter difficulties, illustrated in the following code in which I don't know how to replace the last sorry:

import measure_theory.lp_space

open measure_theory
open_locale ennreal

variables {α E : Type*} [measurable_space α] {p : 0} {μ : measure α}
  [measurable_space E] [normed_group E] [borel_space E]
  [topological_space.second_countable_topology E] [complete_space E]

lemma complete_space_Lp_of_ne_top [hp : fact(1  p)] (hp_ne_top : p  ) :
  complete_space (Lp E p μ) := sorry

lemma complete_space_Lp_top : complete_space (Lp E  μ) := sorry

lemma complete_space_Lp [hp : fact(1  p)] : complete_space (Lp E p μ) :=
begin
  by_cases hp_top : p = ,
  { have h_eq : Lp E p μ = Lp E  μ, by rw hp_top,
     -- I want to use `complete_space_Lp_top`
    sorry },
  { exact complete_space_Lp_of_ne_top hp_top, },
end

I can prove complete_space (Lp E ∞ μ), but I cannot find a way to get complete_space (Lp E p μ) from that and p = ∞.

Sebastien Gouezel (Feb 10 2021 at 17:33):

import measure_theory.lp_space

open measure_theory
open_locale ennreal

variables {α E : Type*} [measurable_space α] {p : 0} {μ : measure α}
  [measurable_space E] [normed_group E] [borel_space E]
  [topological_space.second_countable_topology E] [complete_space E]

lemma complete_space_Lp_of_ne_top [hp : fact(1  p)] (hp_ne_top : p  ) :
  complete_space (Lp E p μ) := sorry

lemma complete_space_Lp_top : complete_space (Lp E  μ) := sorry

lemma complete_space_Lp [hp : fact(1  p)] : complete_space (Lp E p μ) :=
begin
  by_cases hp_top : p = ,
  { convert complete_space_Lp_top,
    apply_instance },
  { exact complete_space_Lp_of_ne_top hp_top, },
end

When you have something which looks like your goal, but in which some things are different from your goal, use convert: it will only leave you with proof goals saying that the things that look different are in fact the same.

Rémy Degenne (Feb 10 2021 at 17:35):

Thank you! I keep forgetting about that tactic.


Last updated: Dec 20 2023 at 11:08 UTC