CompactIccSpace for unitInterval

Stream: new members

[Robert hackman]

So I've been trying for ages to solve this.
I only need need to proof now that there is

instance : CompactIccSpace unitInterval := by
  unfold unitInterval
  apply CompactIccSpace.mk'
  intro b
  intro c
  intro d
  rw[isCompact_iff_compactSpace]

⊢ CompactSpace ↑(Set.Icc b c)
But I can't any proof for that, nor for isCompact. I really desperate for help, I spend way too much time on that now ):

regards

[Ruben Van de Velde]

A #mwe (with imports) is helpful

[Yaël Dillies]

That doesn't seem too hard. Will give it a stab tonight if nobody beats me to it

[Ruben Van de Velde]

Hint: it takes only two calls to apply? after intro d

[Damiano Testa]

... and there is a proof that is exactly 100 characters long, including the statement! :100:

[Ruben Van de Velde]

I've got a proof in 81 80, if we're counting :)

[Damiano Testa]

Is the 81 vs 80 difference due to => vs ↦? :man_facepalming:

[Ruben Van de Velde]

Oh no, that would bring me down to 79 :)

[Ruben Van de Velde]

proofs

instance : CompactIccSpace unitInterval := ⟨fun {_ _} => isClosed_Icc.isCompact⟩
instance : CompactIccSpace unitInterval := .mk' fun _ => isClosed_Icc.isCompact

[Damiano Testa]

I am still not used to the "anonymous dot-notation".

[Ruben Van de Velde]

To be clear, @Robert hackman , this talk about the number of characters is extremely unimportant, except maybe as a puzzle for people who enjoy it

[Damiano Testa]

Besides being unimportant, it is actually obfuscating and pedagogically wrong, especially at the level where it got to here!

[Robert hackman]

thx so much... I think approaching Lean without having ever touched functional programming was the mistake haha :joy: . The math part really is a peace of cake but I'm lacking the PHD in Type Theory ):

[Ruben Van de Velde]

Fwiw, I did a little bit of functional programming a number of years sago (that I don't care to count right now :)) and I didn't enjoy it at all

[Kevin Buzzard]

@Robert hackman I think the only type theory you ever really need to know, if you just want to do mathematics in Lean, is covered in #tpil .

[Robert hackman]

it's not about the "how" (though it is too) but more about a different way of thinking, I think only experience(or smartness - I don't have) can compensate

[Robert hackman]

but regarding the solution above, what I don't understand is why you can call isCompact on isClosed_Icc because isClosed_Icc returns a proposition and isCompact needs a set to be called on...

[Kevin Buzzard]

If you make a #mwe I can try and help with your question. But honestly, for questions like this you can usually just solve them by hovering over things and thinking "OK so what inputs are round brackets?

[Kevin Buzzard]

Oh, you just mean this?

import Mathlib

instance : CompactIccSpace unitInterval := ⟨fun {_ _} => isClosed_Icc.isCompact⟩

isClosed_Icc returns a proof, not a proposition (which is a statement). Does this help? Do you understand the difference between {} inputs to functions ("Lean will work this out") and () inputs ("the user must supply these")? Honestly I recommend you read #tpil rather than just trying to work out everything yourself by staring at more complex examples.

[Ruben Van de Velde]

The version I came up with from your code was roughly

instance : CompactIccSpace unitInterval := by
  unfold unitInterval
  apply CompactIccSpace.mk'
  intro b
  intro c
  intro d
  apply IsClosed.isCompact
  apply isClosedIcc

If you see how that works, you're 90% of the way there

[Robert hackman]

isClosed_Icc returns a proof, not a proposition (which is a statement).ahhh ok so now it makes sense...I was initially confused about why it returned an instance of itself... thanks! (I will go through tplil again.. )

[Robert hackman]

Ruben Van de Velde said:

The version I came up with from your code was roughly

instance : CompactIccSpace unitInterval := by
  unfold unitInterval
  apply CompactIccSpace.mk'
  intro b
  intro c
  intro d
  apply IsClosed.isCompact
  apply isClosedIcc

If you see how that works, you're 90% of the way there

ok so that also resolves my question, thx!

[Robert hackman]

Ok another small question, when Lean cannot find an instance but I cannot use instance because I'm in a tactic block for example but for the instance proof I need a variable from the tactic block, how can I provide a hin to the type resolution if I cannot use instance. Sure I can use have but that doesn't help lean to find the instance "hint"

[Ruben Van de Velde]

I don't follow the question. Can you share the code?

[Kevin Buzzard]

The best way to ask questions here is via #mwe s

[Robert hackman]

Sorry for the late reply.
My problem is the following:

import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.MeasureTheory.Measure.MeasureSpace
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Mathlib.Topology.ContinuousFunction.Basic

 abbrev C := ContinuousMap unitInterval ℝ
theorem test (f : ℕ → C) (limit : C):  ... := by
   let bound := f n
   let μ: MeasureTheory.Measure unitInterval := volume

   let hint := MeasureTheory.IntegrableOn.integrable (Continuous.integrableOn_Icc (bound.continuous))

which throws:

typeclass instance problem is stuck, it is often due to metavariables
  IsLocallyFiniteMeasure ?m.55068

To solve this I want to declare instance IsLocallyFiniteMeasure on μ. The problem is that the instance keyword only works outside the tactic context but I don't have μ available there. If I do instance : IsLocallyFiniteMeasure (MeasureTheory.Measure unitInterval) := sorry that throws:

application type mismatch
  IsLocallyFiniteMeasure (Measure ↑unitInterval)
argument
  Measure ↑unitInterval
has type
  Type : Type 1
but is expected to have type
  Measure ?m.31956 : Type ?u.31955

First I thought that is because MeasureTheory.Measure unitInterval is not proofed but then I found that Measure does not return prop but a type. Then I thought it would be best to look for volumeand what it does but I couldn't find it in the docs nor in the source code... Now I'm a bit out of ideas again

[Ruben Van de Velde]

Wait wait

[Ruben Van de Velde]

This sounds more like lean can't figure out which type you want to be IsLocallyFiniteMeasure rather than the instance not existing

[Robert hackman]

so what does that mean? :D Do you mean that there is ambiguity in Continuous.integrableOn_Icc (bound.continuous)?

[Robert hackman]

If so, declaring the instance would resolve that wouldn't it?

[Ruben Van de Velde]

Can you share a #mwe that shows the typeclass instance problem is stuck?

[Kevin Buzzard]

I get unexpected token '...'; expected term. Can you make a #mwe @Robert hackman ? We need to be able to see the same thing as you to answer the question properly. Check your example in a new Lean file or the web editor before posting.

[Robert hackman]

Ok so that's a working #mve. It's rather big which is why I didn't post it, but when shrinking it the context is diverted and the error changes.
Also I'm sorry for replying so inconsistently, but I'm currently on a very tight time budget.

import Mathlib.MeasureTheory.Measure.Haar.OfBasis
import Mathlib.Order.Basic
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Topology.ContinuousFunction.Basic
import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.MeasureTheory.Measure.MeasureSpace
import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Topology.UnitInterval
import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Mathlib.Topology.Algebra.Order.Compact

open StronglyMeasurable
open Num
open Group
open Real
open BigOperators
open Topology
open ENNReal
open Finset
open Nat
open NatCast
open Function
open MeasureTheory
open Measure


-- -------------
-- Auf dem Raum der stetigen Funktionen C([0,1]) ist durch ∥f∥L1 = R1|f(x)|dx eine Normdefiniert.
-- (Dies brauchen Sie nicht zu zeigen.) Zeigen Sie, dass eine Funktionenfolge (fn) in C([0, 1]),
-- die gleichma ̈ßig gegen f konvergiert, auch bezu ̈glich der Norm ∥ · ∥L1 gegen f konvergiert.

abbrev C := ContinuousMap unitInterval ℝ

noncomputable
def L1_norm (f : C) : ℝ := ∫ x: unitInterval, |f x|

-- Define the L1 space
def L1 := {f : C | L1_norm f ≥ 0 }

-- Define the uniform convergence
def uniform_convergent (f : ℕ → C) (limit : C) := ∀ ε : ℝ, ε > 0 → ∃ N : ℕ, ∀ n : ℕ, n ≥ N → ∀ x : unitInterval, x ∈ Set.Icc 0 1 → |(f n) x - limit x| < ε

instance : NormedAddCommGroup ℝ := normedAddCommGroup
-- instance : IsLocallyFiniteMeasure (MeasureTheory.Measure unitInterval) := sorry

instance : CompactIccSpace unitInterval := by
  unfold unitInterval
  apply CompactIccSpace.mk'
  intro b
  intro c
  intro d
  apply IsClosed.isCompact
  apply isClosed_Icc

-- Theorem: If (fn) converges uniformly to f, then it also converges in L1 norm to f.
theorem uniform_convergence_implies_L1_convergence (f : ℕ → C) (limit : C) (h_uniform : uniform_convergent f limit) :
  Filter.Tendsto (λ n => L1_norm (f n)) Filter.atTop (𝓝 (L1_norm limit)) := by
    -- We need to show that the L1 norms converge to the L1 norm of the limit
    rw[Metric.tendsto_atTop]
    intros ε ε_pos
    -- Use the uniform convergence property to find N
    obtain ⟨N, hN⟩ := h_uniform ε ε_pos
    use N
    intros n hn
    -- Use the definition of the L1 norm
    unfold L1_norm
    have h₁ : ∀ x ∈ Set.Icc 0 1, |(f n - limit) x| ≤ ε := by
      intros x hx
      specialize hN n hn x hx
      exact (le_of_lt hN)

    -- rw[← L1.dist_eq_integral_dist]

    -- Apply the Lebesgue Dominated Convergence Theorem
    -- integral_le_integral_of_le
    -- exact integral_le_integral_of_le (ContinuousMap.abs_sub_integral_le _ _ h₁)


    let bound := f n
    let μ: MeasureTheory.Measure unitInterval := volume




    let hmeas : ∀n, AEStronglyMeasurable (f n) volume := by
      intro ns
      exact AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable (ContinuousMap.measurable (f ns)))
    -- show vv

    let hint := MeasureTheory.IntegrableOn.integrable (Continuous.integrableOn_Icc (bound.continuous))

    let hbound : ∀ n, ∀ᵐ a ∂μ, ‖f n a‖ ≤ bound a  := sorry
    let hlim : ∀ᵐ a ∂μ, Filter.Tendsto (fun n : ℕ ↦ f n a) Filter.atTop (𝓝 (limit a))  := sorry
    exact tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim

[Damiano Testa]

According to the infoview, bound is a term of C, that is a real number in the unit intervalEDIT: sorry I misread! What should bound.continuous represent? Lean is confused by the fact that you are supplying this for a proof that a function is continuous.

[Ruben Van de Velde]

First step: isolate the thing that goes wrong:

    have := Continuous.integrableOn_Icc (bound.continuous)

If you hover over Continuous.integrableOn_Icc, you can see it requires IsLocallyFiniteMeasure μ which seems likely to have created the goal that lean has trouble with (IsLocallyFiniteMeasure ?m.7695). What happened here is that lean can't tell what μ should be. So you can pass it explicitly:

    have := Continuous.integrableOn_Icc (μ := volume) (bound.continuous)

but this still complains that

failed to synthesize instance
  IsLocallyFiniteMeasure volume

Hovering over volume shows it's the volume for unitInterval. The next thing I'd try is adding

instance : IsLocallyFiniteMeasure (volume (α := unitInterval)) := by
  sorry

and look what happens next. Unfortunately it still can't figure out which Icc you want to talk about, so you can try this:

    have := Continuous.integrableOn_Icc (μ := volume) (a := 0) (b := 1) (bound.continuous)

which allows you to move forward

[Ruben Van de Velde]

This is an awful proof for the instance, which I'm posting hoping that someone will reply with a one-line proof:

instance : IsLocallyFiniteMeasure (volume (α := unitInterval)) := by
  unfold unitInterval
  refine @IsFiniteMeasure.toIsLocallyFiniteMeasure _ _ _ _ ?_
  constructor
  have := Real.isFiniteMeasure_restrict_Icc 0 1
  rw [←MeasurableSet.map_coe_volume] at this
  have := this.measure_univ_lt_top
  convert this
  rw [@volume_set_coe_def]
  rw [comap_subtype_coe_apply]
  rw [map_comap_subtype_coe]
  rw [restrict_apply]
  simp only [Set.image_univ, Subtype.range_coe_subtype, ge_iff_le, zero_le_one, not_true, gt_iff_lt, Set.mem_Icc,
    Set.univ_inter, volume_Icc, sub_zero, ofReal_one]
  rw [Set.Icc_def]
  simp
  simp
  simp
  simp
  simp

[Robert hackman]

thank you very much! I misinterpreted the error and thought that it knew μ but couldn't synthesise the instance on it but it absolutely makes sense now that it couldn't find it

[Robert hackman]

application type mismatch
  tendsto_integral_of_dominated_convergence (↑bound) hmeas hint
argument
  hint
has type
  Integrable ↑bound : Prop
but is expected to have type
  Integrable ↑bound : Prop

Usually I bang my head against a problem until either the problem or my head is gone, and then I ask, but with the next error I get, there is not much to bang against...
Updated MVE would then be:

import Mathlib.MeasureTheory.Measure.Haar.OfBasis
import Mathlib.Order.Basic
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Topology.ContinuousFunction.Basic
import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.MeasureTheory.Measure.MeasureSpace
import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Topology.UnitInterval
import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Mathlib.Topology.Algebra.Order.Compact

open StronglyMeasurable
open Num
open Group
open Real
open BigOperators
open Topology
open ENNReal
open Finset
open Nat
open NatCast
open Function
open MeasureTheory
open Measure

-- -------------
-- Auf dem Raum der stetigen Funktionen C([0,1]) ist durch ∥f∥L1 = R1|f(x)|dx eine Normdefiniert.
-- (Dies brauchen Sie nicht zu zeigen.) Zeigen Sie, dass eine Funktionenfolge (fn) in C([0, 1]),
-- die gleichma ̈ßig gegen f konvergiert, auch bezu ̈glich der Norm ∥ · ∥L1 gegen f konvergiert.

abbrev C := ContinuousMap unitInterval ℝ

noncomputable
def L1_norm (f : C) : ℝ := ∫ x: unitInterval, |f x|

-- Define the L1 space
def L1 := {f : C | L1_norm f ≥ 0 }

-- Define the uniform convergence
def uniform_convergent (f : ℕ → C) (limit : C) := ∀ ε : ℝ, ε > 0 → ∃ N : ℕ, ∀ n : ℕ, n ≥ N → ∀ x : unitInterval, x ∈ Set.Icc 0 1 → |(f n) x - limit x| < ε

instance : NormedAddCommGroup ℝ := normedAddCommGroup
instance : IsLocallyFiniteMeasure (volume (α := unitInterval)) := by sorry

instance : CompactIccSpace unitInterval := by
  unfold unitInterval
  apply CompactIccSpace.mk'
  intro b
  intro c
  intro d
  apply IsClosed.isCompact
  apply isClosed_Icc

-- Theorem: If (fn) converges uniformly to f, then it also converges in L1 norm to f.
theorem uniform_convergence_implies_L1_convergence (f : ℕ → C) (limit : C) (h_uniform : uniform_convergent f limit) :
  Filter.Tendsto (λ n => L1_norm (f n)) Filter.atTop (𝓝 (L1_norm limit)) := by
    -- We need to show that the L1 norms converge to the L1 norm of the limit
    rw[Metric.tendsto_atTop]
    intros ε ε_pos
    -- Use the uniform convergence property to find N
    obtain ⟨N, hN⟩ := h_uniform ε ε_pos
    use N
    intros n hn
    -- Use the definition of the L1 norm
    unfold L1_norm
    have h₁ : ∀ x ∈ Set.Icc 0 1, |(f n - limit) x| ≤ ε := by
      intros x hx
      specialize hN n hn x hx
      exact (le_of_lt hN)

    -- rw[← L1.dist_eq_integral_dist]

    -- Apply the Lebesgue Dominated Convergence Theorem
    -- integral_le_integral_of_le
    -- exact integral_le_integral_of_le (ContinuousMap.abs_sub_integral_le _ _ h₁)


    let bound := f n
    let μ: MeasureTheory.Measure unitInterval := volume




    let hmeas : ∀n, AEStronglyMeasurable (f n) volume := by
      intro ns
      exact AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable (ContinuousMap.measurable (f ns)))
    -- show vv

    let hint := MeasureTheory.IntegrableOn.integrable (Continuous.integrableOn_Icc (μ := volume) (a := 0) (b := 1) (bound.continuous))

    let hbound : ∀ n, ∀ᵐ a ∂μ, ‖f n a‖ ≤ bound a  := sorry
    let hlim : ∀ᵐ a ∂μ, Filter.Tendsto (fun n : ℕ ↦ f n a) Filter.atTop (𝓝 (limit a))  := sorry
    exact tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim

[Ruben Van de Velde]

Hmm, IntegrableOn.integrable introduces a restrict in the measure. Not sure how to deal with that

[Robert hackman]

well, so does that mean my approach is invalid or is it "just a hard problem"?