Proofing convergence

Stream: maths

[Robert hackman]

Hi so I want to use tendsto_integral_of_dominated_convergence. Therefor I need to define a measure on unitInterval. For the hmeasargument, Measure alphais required, so I'm simple defining exactly that. Sadly that returns Type1 which is not Measure alpha. I'm still not trusted at all with the functional type way of thinking about things and quite confused. Could somebody explain what's happening here? Type1 is a type, ok, but what's Measure alpha requiring then, if not a Type or a instance of such..
regards

    let bound := unitInterval → ℝ
    let μ := MeasureTheory.Measure unitInterval

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

[Eric Wieser]

You want let μ : MeasureTheory.Measure unitInterval := sorry, not let μ := MeasureTheory.Measure unitInterval

[Eric Wieser]

The analog is let r : Real := 3.14 vs let r := Real

[Eric Wieser]

If you're lucky, the sorry is volume

[Robert hackman]

thanks! volume works as well. This was obvious again, sry. I was looking at the wrong def of Measurable, wasn't aware that it returns a prop.

[Robert hackman]

I want to proof the following expression:

let hmeas : ∀n, AEStronglyMeasurable (f n) μ := AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable (MeasurableSpace.Top.measurable ((f n) μ) ))

where:

f: ℕ → C
μ: Measure ↑unitInterval := volume

But lean throws the following error:

type mismatch
  AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable (MeasurableSpace.Top.measurable ?m.236751))
has type
  AEStronglyMeasurable ?m.236751 ?m.54280 : Prop
but is expected to have type
  ∀ (n : ℕ), AEStronglyMeasurable (↑(f n)) μ : PropLean 4

It could very well be that I'm approaching completely wrong since I'm completely new to the "less intuitive" analysis part of lean (opposing to the basic algebra stuff...).
For context, I'm trying to proof hmeas in order to proof tendsto_integral_of_dominated_convergence.
I would be so thankful for any help!

[Sebastien Gouezel]

The lemma you are applying is used to prove that a single function is AEStronglyMeasurable. But the statement you are proving is that in a whole family of functions, each of them is AEStronglyMeasurable. You should say that you want to focus on a single function with intro n. This issue has nothing to do with measures, it's a general Lean thing.

[Sebastien Gouezel]

(I know it's quite hard to decipher error message, but the error message you posted is trying to tell you exactly this).

[Robert hackman]

Ok, that's what it looks like now:

    let hmeas : ∀n, AEStronglyMeasurable (f n) μ := by
      intro ns
      exact AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable (MeasurableSpace.Top.measurable ((f ns))))

And It seems more "reasonable" than what I had before but the error it throws is a bit cryptic to me.

Main.lean:104:71
application type mismatch
  Measurable.aemeasurable (MeasurableSpace.Top.measurable ↑(f ns))
argument
  MeasurableSpace.Top.measurable ↑(f ns)
has type
  @Measurable ↑unitInterval ℝ ⊤ Real.measurableSpace ↑(f ns) : Prop
but is expected to have type
  @Measurable ↑unitInterval ℝ Subtype.instMeasurableSpace Real.measurableSpace ↑(f ns) : Prop

[Ruben Van de Velde]

Looks like MeasurableSpace.Top.measurable is not the right expression to write there

[Robert hackman]

ok, because the signature returns Measurable f....

[Sebastien Gouezel]

Can you give a #mwe?

[Robert hackman]

Sure, this is a bit of a mess though... I want to proof that C 0 1 is also uniform convergent to f with the L1 norm.. The last lemma tendsto_integral_of_dominated_convergenceis (hopefully) proofing that through the assumption that it's uniform convergent without the integral as well.

import Mathlib.Topology.ContinuousFunction.Basic
import Init.Core
import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.MeasureTheory.Measure.MeasureSpace
import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Data.Real.ENNReal
import Mathlib.MeasureTheory.Measure.Haar.OfBasis
import Mathlib.Topology.UnitInterval
import Mathlib.Topology.Basic
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Analysis.Normed.Group.Completion
import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

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

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
-- 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 := limit
    let μ: MeasureTheory.Measure unitInterval := volume

    -- let hmeas : ∀n, AEStronglyMeasurable (f n) μ := by
    --   intro ns
    --   exact AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable (MeasurableSpace.Top.measurable ((f ns))))

    have l : MeasureTheory.IntegrableOn bound (Set.Icc 0 1) μ := sorry
    let hint : Integrable bound μ := MeasureTheory.IntegrableOn.integrable l

    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]

For your specific question:

    let hmeas : ∀n, AEStronglyMeasurable (f n) volume := by
      intro ns
      refine AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable ?_)
      apply? says
        exact ContinuousMap.measurable (f ns)

[Robert hackman]

Ruben Van de Velde said:

For your specific question:

    let hmeas : ∀n, AEStronglyMeasurable (f n) volume := by
      intro ns
      refine AEMeasurable.aestronglyMeasurable (Measurable.aemeasurable ?_)
      apply? says
        exact ContinuousMap.measurable (f ns)

thanks so much... to me this is still black magic :fire: I will need some time working though it