Portmanteau theorem

Stream: new members

[Kalle Kytölä]

To learn Lean and mathlib, I played through my own sequel to the NNG, and formalized the proof of the Portmanteau theorem on equivalent characterizations of weak convergence.

I have so far deliberately not asked whether more serious people have already done that; I noticed earlier that knowing it made the game less fun for me (since my progress was slower and the result clumsier). But now that I played through the part that I had set as my goal, I would be very happy to hear expert views on how weak convergence and Portmanteau theorem should have been done and what is their status in mathlib.

I will have a few specific questions here... For reference, here is my Portmanteau game-play. (It will not be hard to recognize as a stubborn beginner's attempt --- especially with some trivial lemmas stated in a lousy generality and having ridiculously lengthy proofs).

But more generally, although I am obviously not yet able to write clean Lean of mathlib standards on my own, I feel like with the first exercise out of the way I could soon start slowly contributing somewhere...

[Kalle Kytölä]

The main statement of my formalization of the Portmanteau theorem in metric spaces looks like the following (sorry, not self-contained, needs a few imports from other files, but should give a fair picture). You should be able to decide from a comparison of wikipedia and the code below whether I actually formalized a fair approximation to the right result :wink:...

/-- `tfae_weak_conv_seq` :
    Equivalent conditions for the weak convergence of a sequence of Borel probability
    measures on a metric space. -/
theorem tfae_weak_conv_seq {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tfae  [ tendsto μseq at_top (𝓝 μ) ,
            ∀ (f : α → ℝ) , continuous f → bdd_Rval f →
              tendsto (λ n, (@integral α ℝ (borel(α)) _ _ _ _ _ _ (μseq(n)) f)) at_top (𝓝 (@integral α ℝ (borel(α)) _ _ _ _ _ _ μ f)) ,
            ∀ (f : cont_bdd_ennval α) ,
              tendsto (λ n, integrate_cont_bdd_ennval (μseq(n)) f) at_top (𝓝 (integrate_cont_bdd_ennval μ f)) ,
            ( ∀ (G : set α) , (is_open G) → μ(G) ≤ liminf at_top (λ n , (μseq(n))(G)) ) ,
            ( ∀ (F : set α) , (is_closed F) → limsup at_top (λ n , (μseq(n))(F)) ≤ μ(F) ) ,
            ( ∀ (E : set α) , (borel_set(α) E) → (μ(frontier E) = 0) → (tendsto (λ n , (μseq(n))(E)) at_top (𝓝 (μ(E))) ) ) ] := by sorry

[Kalle Kytölä]

I guess one part which I in the end actually felt satisfied about was the very definition of the topology on the "set" of Borel probability measures on a topological space. I felt that the definition was relatively succinct (by my standards) and building on existing mathlib. Since I managed to prove (in a clumsy but sorry-free way) its equivalence with the usual conditions, I think it is not absolutely wrong (might be a bad implementation, of course!)... One choice I was happy about was to use ennreal-valued functions and lintegrals instead on real-valued functions and Bochner-integrals in the definition of the topology (the equivalence to usual is anyway proven later).

But ok... What is the experts' verdict on the following definition?

import tactic
import measure_theory.measurable_space
import measure_theory.integration
import measure_theory.borel_space
import measure_theory.bochner_integration
import topology.metric_space.basic
import topology.instances.real
import topology.instances.ennreal
import order.liminf_limsup

noncomputable theory
open set
open classical
open measure_theory
open measurable_space
open filter
open_locale topological_space

abbreviation bdd_ennval {α : Type*} (f : α → ennreal) : Prop :=
  ∃ (M : nnreal) , ∀ (a : α) , f(a) ≤ M

/-- Continuous bounded functions on a topological space `α` with values
in `ennreal` are used as "test functions" in the definition of the topology of
the weak convergence of probability measures. They are defined as a subtype
of `α → ennreal`, so that the type of (positive) functionals is just
`(cont_bdd_ennval α) → ennreal`. -/
def cont_bdd_ennval (α : Type*) [topological_space α] : Type*
  := { f : α → ennreal // continuous f ∧ bdd_ennval f }

def functional_cont_bdd_ennval (α : Type*) [topological_space α] : Type*
  := (cont_bdd_ennval α) → ennreal

instance {α : Type*} [topological_space α] :
  has_coe (cont_bdd_ennval α) (α → ennreal) := ⟨subtype.val⟩

@[simp] lemma val_eq_coe_testfun {α : Type*} [topological_space α] (f : cont_bdd_ennval α) :
  f.val = f := rfl

/-- As a first step towards the definition of the topology of the weak convergence
of probability measures, the space of functionals `(cont_bdd_ennval α) → ennreal`
is equipped with the product topology (the topology of "testfunctionwise" convergence,
i.e., of pointwise convergence of the functionals defined on the space of continuous
bounded test functions). -/
instance {α : Type*} [topological_space α] :
  topological_space (functional_cont_bdd_ennval α) := Pi.topological_space

/-- Borel probability measures on a topological space `α` are defined as a subtype
of measures. This subtype `borel_proba α` is equipped with the topology of weak
convergence. -/
def borel_proba (α : Type*) [topological_space α] : Type
  := { μ : @measure_theory.measure α (borel(α)) // @probability_measure α (borel(α)) μ }

instance (α : Type*) [topological_space α] :
  has_coe (borel_proba α) (@measure_theory.measure α (borel(α))) := ⟨subtype.val⟩

@[simp] lemma val_eq_coe_borel_proba {α : Type*} [topological_space α] (ν : borel_proba α) :
  ν.val = ν := rfl

abbreviation integrate_cont_bdd_ennval {α : Type*} [topological_space α]
  (μ : borel_proba α) (f : cont_bdd_ennval α) : ennreal := @lintegral α (borel(α)) μ f

/-- The topology of weak convergence on `borel_proba α` is defined as the induced
topology of the mapping `(borel_proba α) → ((cont_bdd_ennval α) → ennreal)` to
functionals defined by integration of a test functio against to the measure. In
other contexts this could be called the weak-* topology. -/
instance {α : Type} [topological_space α] : topological_space (borel_proba α)
  := topological_space.induced (λ (μ : borel_proba α) , integrate_cont_bdd_ennval μ) infer_instance

/-- Integration of test functions against borel probability measures depends
continuously on the measure. -/
lemma integrate_cont_bdd_ennval_cont {α : Type} [topological_space α] :
  continuous (@integrate_cont_bdd_ennval α _) := continuous_induced_dom

lemma conv_seq_induced {α γ : Type*} [top_γ : topological_space γ]
  (f : α → γ) (x : ℕ → α) (x₀ : α) :
    tendsto (f ∘ x) at_top (𝓝 (f(x₀)))
      → tendsto x at_top (@nhds α (topological_space.induced f top_γ) x₀) :=
begin
  intro h_f_lim ,
  apply tendsto_nhds.mpr ,
  intros U open_U U_ni_x₀ ,
  rcases ((@is_open_induced_iff α γ top_γ U f).mp open_U) with ⟨ V , open_V , preim_V_eq_U ⟩ ,
  induction preim_V_eq_U ,
  apply tendsto_nhds.mp h_f_lim V open_V U_ni_x₀ ,
end

/-- The usual definition of weak convergence of probability measures is given in
terms of sequences of probability measures: it is the requirement that the integrals
of all continuous bounded functions against members of the sequence converge.
This characterization is shown in `weak_conv_seq_iff'` in the case when the
functions are `ennreal`-valued and the integral is `lintegral`. The most common
formulation with `ℝ`-valued functions and Bochner integrals is `weak_conv_seq_iff`. -/
theorem weak_conv_seq_iff' {α : Type*} [topological_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ ∀ (f : cont_bdd_ennval α) ,
        tendsto (λ n, integrate_cont_bdd_ennval (μseq(n)) f) at_top (𝓝 (integrate_cont_bdd_ennval μ f)) :=
begin
  split ,
  { intros weak_conv ,
    have key := tendsto.comp (continuous.tendsto (@integrate_cont_bdd_ennval_cont α _) μ) weak_conv ,
    exact tendsto_pi.mp key , } ,
  { intro h_lim_forall ,
    have h_lim : tendsto (λ n, integrate_cont_bdd_ennval (μseq(n))) at_top (𝓝 (integrate_cont_bdd_ennval μ)) ,
    { exact tendsto_pi.mpr h_lim_forall , } ,
    exact conv_seq_induced _ μseq μ h_lim , } ,
end

[Kevin Buzzard]

I have no idea about whether this stuff is already in lean but very well done regardless!

[Filippo A. E. Nuccio]

Very nice! I also notice that you use abbreviation, which I was not aware of. Have you found some sort of "general" Lean documentation or have you been looking around mathlib for inspiration?

[Kalle Kytölä]

I think I picked abbreviation up from this Zulip, but I don't remember for sure... It felt convenient, since the statements of the equivalent conditions (as well as some frequently used definitions) were a bit long and often repeated otherwise.

But in the end I'm not sure abbreviations are good style: they are probably syntactically different (computer literate people, please correct me if I'm wrong) than the actual thing that is being abbreviated, so they are not directly recognized by Lean when applying results. One needs to unfold somehow or resort to things in which definitional equality suffices (again, please correct me if this is rubbish). For this reason I actually already started to remove some of the ones I had in earlier versions... [EDIT: This seems to be wrong, see Patrick's answer below.]

I originally used defs instead. To be honest, I don't know what is the difference :laughter_tears:. I think I just tried abbreviation and hoped it would improve some things, and I'm not sure it did in the end...

Actually I would be very happy to hear about recommendations on the use or avoidance of abbreviations and/or defs from experienced users!

[Patrick Massot]

I think abbreviations are purely a parsing and pretty-printing thing, so they don't block anything. Compare:

abbreviation Nat := nat

example (x : Nat) : x + 0 = x := nat.add_zero x

def Nat' := nat

example (x : Nat') : x + 0 = x := nat.add_zero x
-- failed to synthesize type class instance for has_zero Nat'

[Kalle Kytölä]

Ok, I think I was hoping for something like that, but occasionally felt I needed to do extra steps to somehow unfold (although not with unfold). I think in the end I was just a bit confused...

Thanks Patrick for the accurate information and example!

[Eric Wieser]

Don't abbreviations block rewrites?

[Eric Wieser]

Ah, here's what I'm thinking of:

abbreviation Nat := nat

abbreviation zero_add := (+) 0

example (x : Nat) : x + 0 = x := begin
  rw nat.add_zero,
end

example (x : Nat) : zero_add x = x := begin
  -- dunfold zero_add, -- works with this
  rw nat.zero_add, -- fails
end

abbreviation for types are basically fully transparent, abbreviations for functions are not.

[Filippo A. E. Nuccio]

I see, but my question was more about you having found a comprehensive Lean documentation, rather than this specific issue!

[Kalle Kytölä]

Regarding comprehensive documentation I don't unfortunately have better suggestions than are on the learning resources page. I just banged my head against the portmanteau until I got the goals accomplished! :tada:. The most frequent technique was to (recursively) right-click on a term of interest and follow the Go to Definition link to the right file in mathlib. This Zulip is obviously also great (although I deliberately did not make use of it for my first exercise).

Thanks Eric and Patrick for the insight into abbreviation (you answered at least questions I had about it).

[Bryan Gin-ge Chen]

This is really impressive work, especially for a first project! I think @Floris van Doorn is one of our local measure theory experts.

[Kalle Kytölä]

Do I remember correctly that Fubini's theorem is by @Floris van Doorn? (Apologies if I misattribute, and in any case thanks a lot to whoever did it!)

Maybe I'd ask if the following application of Fubini had been done before (this is in my portmanteau_open_imp_cont.lean):

lemma lintegral_eq_lintegral_ccdf {β : Type*} [measurable_space β]
  (μ : measure β) [hμ : sigma_finite μ] (g : β → ennreal) [hg : measurable g] :
    lintegral μ g = lintegral (volume.restrict { t : ℝ | 0 < t } : measure ℝ) (λ (t : ℝ) , μ (g ⁻¹' Ioi (ennreal.of_real t)) ) := by sorry

It is very frequently used in probability theory.

[Heather Macbeth]

Yes, Floris did Fubini! I wonder if you could get this lemma by combining
docs#volume_region_between_eq_lintegral
(to get that lintegral μ g is the volume under the curve g in β × ℝ) with
docs#measure_theory.measure.prod_apply
(to get that that volume is equal to the integral on your right-hand side).

I'm not an expert on the measure theory library, but I don't think we have this lemma directly.

[Heather Macbeth]

In any case, I think it would be a good addition to the library!

[Kalle Kytölä]

Thanks Heather! Those results are of course very closely related to the one I asked about.

I didn't yet try to reduce my proof to the theorems you mention. The first reason is that the pen-and-paper proof of the result is so short (a couple of lines) starting from Fubini itself that it feels nothing else but docs#lintegral_lintegral_swap should be needed. Of course the extra stuff that is needed (yeah, who could have guessed) is mostly measurability questions, and it might be that those could have been simplified by existing results. However, there is a minor difference in the choice of the codomain anyway, as I preferred values in ennreal whereas the results you quote had ℝ, so it was unclear to me if measurability proofs would be shortened by applying them... (Moreover, I didn't yet exactly try to optimize my proofs :grinning_face_with_smiling_eyes:). It is worth noting though that much of the pain in my approach was that while doing measurability things in ennreals, I had to use a custom < (namely real_lt_ennreal). I think this is likely a dubious design choice responsible of much of the mess.

(Incidentally, I just realized that in my own course I state the corresponding result for nnreal-valued functions, probably so that there is a slick measurability trick using subtraction. Subtraction in ennreals, by contrast, was one of the most painful details in the portmanteau exercise.)

Thank you again, I'll think about this some more. If I get a decent version I could try to PR this (or even smaller pieces) to mathlib. :open_mouth:

[Jeremy Avigad]

In case it is helpful, here is the portmanteau theorem in Isabelle: https://isabelle.in.tum.de/dist/library/HOL/HOL-Probability/Weak_Convergence.html. It's also described here on page 35: https://arxiv.org/pdf/1405.7012.pdf.

[Kalle Kytölä]

Thank you! I didn't know of this. I have never read Isabelle code before, but will take a look.

[Kalle Kytölä]

Actually, from the link and paper above (p. 25, it seems) I get the impression that weak convergence in Isabelle was defined for the real line --- I don't find portmanteau for general metric spaces (of course I'm Isabelle-illiterate). Is this accurate or am I missing something? (I didn't do the ℝ-specific equivalent conditions at all yet.)

In any case, if I have the attention of a probability-formalization-pioneer, could you tell me what you think of my definition of the topology of weak convergence as an induced topology? Does this seem like a reasonable implementation? Thanks in advance!

[Kalle Kytölä]

Back to lintegral_eq_lintegral_ccdf briefly...

To make this lintegral_eq_lintegral_ccdf more complementary to the existing theorems pointed out by Heather above (although I'd still believe even the original formulation is useful), I might try to generalize a bit. Specifically, in probability theory, for example to characterize the "decay rate" of cumulative distribution functions of non-negative random variables in $L^p(\mu)$, one uses

$$\int_\Omega f(\omega)^p \, \mathrm{d} \mu(\omega) = p \, \int_0^\infty t^{p-1} \, \mu \big\{ \omega \in \Omega \; \big| \; f(\omega) > t \big\} \, \mathrm{d} t.$$

I guess it is no harder to prove that for any increasing differentiable $\phi : [0,\infty] \to [0,\infty]$ with $\phi(0)=0$ and a non-negative $f$, we have

$$\int_\Omega \phi \big(f(\omega) \big) \, \mathrm{d} \mu(\omega) = \int_0^\infty \phi'(t) \, \mu \big\{ \omega \in \Omega \; \big| \; f(\omega) > t \big\} \, \mathrm{d} t.$$

In fact this is what I originally planned in my exercise, but ran into formalization difficulties (forgot what exactly), so eventually settled for whatever pedestrian version was sufficient for portmanteau...

Of course I'd still like to know if this exists already and is considered mathlib-worthy before taking on the old difficulties...

[Heather Macbeth]

I also think it would be nice to have a version of docs#volume_region_between_eq_lintegral for nnreal target (perhaps a version without subtraction, doing "region under" rather than "region between"). And this would unify more nicely with docs#measure_theory.measure.prod_apply to produce your theorem in the form you stated it.

[Heather Macbeth]

Kalle Kytölä said:

I guess it is no harder to prove that for any increasing differentiable $\phi : [0,\infty] \to [0,\infty]$ with $\phi(0)=0$ and a non-negative $f$, we have

$$\int_\Omega \phi \big(f(\omega) \big) \, \mathrm{d} \mu(\omega) = \int_0^\infty \phi'(t) \, \mu \big\{ \omega \in \Omega \; \big| \; f(\omega) > t \big\} \, \mathrm{d} t.$$

Yes! This is a very useful fact! I wonder if there is a standard name for it?

[Kalle Kytölä]

The only one I am aware of is that_Fubini_trick_with_complementary_cumulative_distribution_functions. :thinking:

[Heather Macbeth]

Ah ... the "layer cake representation"

[Heather Macbeth]

(in Lieb-Loss Analysis, at least)

[Patrick Massot]

Isn't this what is called Cavalieri's principle?

[Patrick Massot]

It's crucial when $\phi = \mathrm{id}$ since it proves that, in Lebesgue theory, integrating functions is equivalent to measuring sets (if you already have the Riemann integral).

[Patrick Massot]

Random google search to support my claim returns https://math.stackexchange.com/a/158989/207864

[Jeremy Avigad]

@Kalle Kytölä I am far from an expert here. Luke, Johannes, and I were fixated on the CLT, and we just did what we had to do; we followed Billingsley pretty closely. It would be great to do the portmanteau theorem in full generality. Your definition looks very nice to me.

[Kalle Kytölä]

Btw, I think what I have is more or less the full generality that works in metric/metrizable spaces (and in topological spaces, but that statement is not very strong anyway). I guess in metric spaces one could still add the extra condition that it is enough to use Lipschitz test functions (this is basically done inside the proofs, but not in the current version of the statements).

For the special case of $\R$, there are the two additional very useful characterizations that I didn't touch yet:

• by cumulative distribution functions (cdf)
• by characteristic functions.

The cdf version should be a minor addition. The characteristic function version requires more: both a tightness argument (at least Helly's selection theorem) and some Fourier analysis of measures (say Lévy's inversion theorem). I don't know what is the status of Fourier analysis and complex analysis for the latter. For the tightness, my own preferred route would be a long winded one (not the shortcut using Helly's theorem): first have Riesz-Markov-Kakutani representation theorem, then Prokhorov's theorem built on it (much more general than Helly's theorem). By my estimate that is a huge amount of work, though... (Unless someone tells me we have Fourier analysis of measures and Riesz-Markov-Kakutani...)

(Btw, I have kind of also been following Billingsley indirectly, since that was a major source I used for a course I've given since 7 years or so... One of the editions of Billingsley has a proof of Prokhorov's theorem close in spirit to my preferred route, but in other editions he resorts to a common trick that is not my favorite...)

[Heather Macbeth]

Indeed, there is so much to do! :)

I am just glancing over your code to see what might be good starting points for getting these results into mathlib. Your definition cont_bdd_Rval -- can you use docs#bounded_continuous_function instead?

[Heather Macbeth]

Then we already have the normed-space instance, docs#bounded_continuous_function.normed_space, and can get the dual, docs#normed_space.dual, mentioned in your TODO -- I don't know if that helps with anything else

[Kalle Kytölä]

Thanks, this is great info! (Sort of to the direction of Riesz-Markov-Kakutani, exactly as I wanted...)

I'll try it out, but not today unfortunately...

[Heather Macbeth]

It would be wonderful to have Riesz-Markov-Kakutani in mathlib! If I remember correctly, it might be done in Mizar.

[Kalle Kytölä]

Yeah, it would... I will not take it on immediately, though :grinning_face_with_smiling_eyes:. (Who knows, one day...)

[Heather Macbeth]

Do you have a definition of signed measure? Or do you have a workaround allowing you to consider only "standard" (i.e., nonnegative) measures?

[Kalle Kytölä]

Ah, I did not think about the details of the implemetation of that at all... Without thinking I would imagine that one starts by proving that positive functionals correspond to (ordinary) measures. The dual of the normed space would then require building from that. But I haven't actually thought about how I would do it...

[Heather Macbeth]

Ah, here is the Mizar result, but it's only for the dual of continuous functions on intervals in $\mathbb{R}$.

[Heather Macbeth]

https://www.fm.mizar.org/2017-25/pdf25-3/dualsp05.pdf

[Kalle Kytölä]

Actually for Prokhorov's theorem one only essentially needs the positive functionals anyway, not the dual of the normed space version of Riesz-Markov-Kakutani. (It is btw enough to do in compact spaces, one does not need locally compact to work towards Prokhorov in full generality.)

[Heather Macbeth]

Actually, while we are speculating wildly, isn't it true that Riesz-Markov-Kakutani is a main ingredient in constructing Wiener measure?

[Heather Macbeth]

We have some of the other preliminaries, for example Stone-Weierstrass.

[Kalle Kytölä]

I guess there are a few different constructions of the Wiener measure...

One way is via Kolmogorov's extension theorem (I'd have to think what else it eats, might be the least heavy in any case). Another is to prove that the scaling limit of random walks exists, and this requires a Prokhorov in a good generality (so in particular I'd say Riesz-Markov-Kakutani).

[Kalle Kytölä]

Good point, Prokhorov also needs Stone-Weierstrass and a version of Alaoglu in addition to Riesz-Markov-Kakutani in the approach I had in mind...

[Kalle Kytölä]

Ok, fun to speculate wildly after just having only defined weak convergence. :rolling_on_the_floor_laughing: Down this route is a constructive field theory approach to Yang-Mills, I guess :stuck_out_tongue_wink:.

Thanks for the really helpful comments again! I'll work on something some time, almost surely...

[Heather Macbeth]

I hope you will PR this material! :)

[Heather Macbeth]

It's probably bed-time for you but I was just going to say that I now understand what you were saying about choosing ennreal rather than real.

[Heather Macbeth]

Is the point that, eg, in this docstring

/-- The topology of weak convergence on `borel_proba α` is defined as the induced
topology of the mapping `(borel_proba α) → ((cont_bdd_ennval α) → ennreal)`

you need to consider, not the "usual" dual of bounded continuous functions, but a kind of "semigroup" dual with only positive-valued functions.

[Kalle Kytölä]

Yes, I "need" (or rather chose, for good or bad) to do so, because I felt lintegral was simpler than Bochner integral... I'm happy to hear whether that was a good idea :grinning_face_with_smiling_eyes:.

[Heather Macbeth]

Actually, it seems like docs#continuous_linear_map is defined for monoid targets, with semirings of scalars.

[Heather Macbeth]

So you could define the dual to consist of the continuous_linear_map from bounded_continuous_function to ennreal, with ennreal scalars, if I understand correctly?

[Kalle Kytölä]

Ok, thanks for yet another very interesting observation!. But now I'll have to go to sleep :in_bed:. (I already slept too little yesterday after trying to get the existing sorry-free version in github :laughter_tears:)

[Bryan Gin-ge Chen]

Kalle Kytölä said:

Ok, thanks for yet another very interesting observation!. But now I'll have to go to sleep :in_bed:. (I already slept too little yesterday after trying to get the existing sorry-free version in github :laughter_tears:)

I would not be surprised if most of us have had similar experiences! (I can certainly remember a few nights where I looked up from VS Code and it was suddenly 3-4 hours later than I thought it was...)

[Floris van Doorn]

This looks great! It would be really nice to have this in mathlib.

Here are some comments about the code snippet in OP.

import measure_theory.bochner_integration

open measure_theory

-- I would generalize `bdd_ennval` to something like this
def bounded_above {α β : Type*} [has_le β] [has_top β] (f : α → β) : Prop :=
  ∃ (M : β) , M ≠ ⊤ ∧ ∀ (a : α) , f(a) ≤ M

/- I would define the subtype of probability measure in general. (maybe this def should
be called `probability_measure` and the class should be called `is_probability_measure`)
-/
def probability_measures (α : Type*) [measurable_space α] : Type :=
{ μ : measure α // probability_measure μ }

/- the usual way to talk about the borel σ-algebra is as follows. But as long as you don't need it,
don't add the `borel_space` assumption yet. -/
example (α : Type*) [measurable_space α] [topological_space α] [borel_space α] {U : set α}
  (h : is_open U) : measurable_set U :=
h.measurable_set

[Kalle Kytölä]

These suggestions look like clear improvements, thanks Floris!

[Kalle Kytölä]

Actually, to do my first exercise of PRing, I could just try to fix the docstring of docs#measurable_space.comap. It has the following tiny misprint:

The reverse image of a measure space measurable space under a function. comap f m contains the sets s : set α such that s is the f-preimage of a measurable set in β.

I'd also soon try to find some first microscopic parts of the portmanteau project and do the suggested improvements and start PRing them.

Could I get the invite to push to non-master branches of mathlib (or whatever is the appropriate to do this kind of stuff)? Thanks!

[Kevin Buzzard]

What is your github userid?

[Kalle Kytölä]

Oh sorry :flushed:. I think it is simply kkytola, but I actually could not find it in my github profile.

Sorry, I'm very new to computer stuff. This is one of the reasons I wanted to start with the first PRs being sufficiently simple... I would not want to break mathlib. :speechless: :innocent:

Thanks in advance!

[Johan Commelin]

@Kalle Kytölä https://github.com/leanprover-community/mathlib/invitations

[Kalle Kytölä]

Thanks a lot Johan!

(For the record, I've never in my life done a PR, but I hope I'll learn that by this weekend... I'll look into the learning resources first.)

[Johan Commelin]

@Kalle Kytölä did you see the video tutorial on making mathlib PRs?

[Kalle Kytölä]

This video tutorial? I probably saw it on my binge watch streak of Lean YouTube videos earlier, but I will watch it in slow motion again to learn the moves.

[Johan Commelin]

@Kalle Kytölä exactly, that's the one I had in mind

[Johan Commelin]

@Alex Zhang :up: this video might also be useful for you

[Johan Commelin]

It's about making a PR to mathlib

[Kalle Kytölä]

Sorry for the long silence... :speechless: First the progress update: with the help of Heather and Bryan, and after having watched the masterpiece thriller Making a pull request to mathlib by Scott, I managed to make my first PR to a docstring. Big thanks to all of you!

My goal was to continue with PR's, by splitting my original code in infinitesimal pieces and trying to rewrite the pieces to mathlib-quality one by one. Predictably, this was harder than I predicted :grimacing: (in addition to the equally predictable circumstances of having less time than predicted).

[Kalle Kytölä]

I originally thought a cleaned-up version of lintegral_eq_lintegral_ccdf might have been a good first piece of code to PR. But I have so far both failed to simplify my proof in any meaningful way (despite the fact that the lemmas pointed out by Heather seem obviously relevant) and I have even failed to satisfactorily state the generalization I wanted (the one known as either the "layer cake representation" or "Cavalieri's principle")... :dizzy:

I would therefore like try to start from something even simpler.

I of course plan to return to discussing layer cakes in due time...

[Kalle Kytölä]

So what I believe I was partially successful with is trying to take into account the comments (by Floris in particular) that I got regarding the definition of weak convergence. The updated code of the definition piece is below. Does it make sense to PR this piece, and address any further issues with it in the PR process? The definition of the topology would seem like a natural starting point.

The main reason I think it is not a hopeless attempt is that I have the sorry-free (but ugly) proof of Portmanteau theorem from my original definition, which is essentially equivalent. And in fact this definition piece already contains the proof of equivalence with the most obvious one of the conditions.

import measure_theory.bochner_integration

noncomputable theory

open measure_theory
open filter
open_locale topological_space
open_locale bounded_continuous_function


def bounded_above {α β : Type*} [has_le β] [has_top β] (f : α → β) : Prop :=
  ∃ (M : β) , M ≠ ⊤ ∧ ∀ (a : α) , f(a) ≤ M


namespace portmanteau


section test_functions_for_weak_convergence


universes u

/-- Continuous bounded functions on a topological space `α` with values
in `ennreal` are used as "test functions" in the definition of the topology of
the weak convergence of probability measures. They are defined as a subtype
of `α → ennreal`, so that the type of (positive) functionals is just
`(cont_bdd_ennval α) → ennreal`. -/
def cont_bdd_ennval (α : Type*) [topological_space α] : Type*
  := { f : α → ennreal // continuous f ∧ bounded_above f }

instance cont_bdd_ennval.coe (α : Type*) [topological_space α] :
  has_coe (cont_bdd_ennval α) (α → ennreal) := ⟨subtype.val⟩

lemma continuous_of_cont_bdd_ennval {α : Type*} [topological_space α] (f : cont_bdd_ennval α) :
    continuous (f : α → ennreal) := f.prop.1

lemma borel_measurable_of_cont_bdd_ennval {α : Type*}
  [measurable_space α] [topological_space α] [borel_space α] (f : cont_bdd_ennval α) :
    measurable (f : α → ennreal)
      := continuous.measurable (continuous_of_cont_bdd_ennval f)

@[simp] lemma val_eq_coe_cont_bdd_ennval {α : Type*} [topological_space α] (f : cont_bdd_ennval α) :
  f.val = f := rfl

structure bounded_continuous_function_to_ennreal
  (α : Type*) [topological_space α] extends continuous_map α ennreal :=
    (bounded_above' : bounded_above to_fun)

def functional_on_bounded_continuous_function_to_ennreal
  (α : Type*) [topological_space α] : Type*
    := (bounded_continuous_function_to_ennreal α) → ennreal

instance bounded_continuous_function_to_ennreal.has_coe_to_fun
  {α : Type*} [topological_space α] :
    has_coe_to_fun (bounded_continuous_function_to_ennreal α) :=
      ⟨λ _ , α → ennreal, λ f , f.to_fun⟩

instance functional_on_bounded_continuous_function_to_ennreal.has_coe_to_fun
  {α : Type*} [topological_space α] :
    has_coe_to_fun (functional_on_bounded_continuous_function_to_ennreal α) :=
      ⟨λ _ , (bounded_continuous_function_to_ennreal α) → ennreal, λ φ , φ⟩

/-- As a first step towards the definition of the topology of the weak convergence
of probability measures, the space of functionals `(cont_bdd_ennval α) → ennreal`
is equipped with the product topology (the topology of "testfunctionwise" convergence,
i.e., of pointwise convergence of the functionals defined on the space of continuous
bounded test functions). -/
instance {α : Type*} [topological_space α] :
  topological_space (functional_on_bounded_continuous_function_to_ennreal α)
    := Pi.topological_space


end test_functions_for_weak_convergence



section topology_of_weak_convergence


/-- Borel probability measures on a topological space `α` are defined as a subtype
of measures. This subtype `borel_proba α` is equipped with the topology of weak
convergence. -/
def probability_measures (α : Type*) [measurable_space α] : Type
  := { μ : measure α // probability_measure μ }

instance probability_measures.coe (α : Type*) [measurable_space α] :
  has_coe (probability_measures α) (measure_theory.measure α) := ⟨subtype.val⟩

@[simp] lemma val_eq_coe_probability_measures {α : Type*} [measurable_space α] (ν : probability_measures α) :
  ν.val = ν := rfl

abbreviation integrate_cont_bdd_ennval {α : Type*} [measurable_space α] [topological_space α] [borel_space α]
  (μ : probability_measures α) (f : cont_bdd_ennval α) : ennreal := lintegral (μ : measure_theory.measure α) f

/-- The topology of weak convergence on `borel_proba α` is defined as the induced
topology of the mapping `(borel_proba α) → ((cont_bdd_ennval α) → ennreal)` to
functionals defined by integration of a test functio against to the measure. In
other contexts this could be called the weak-* topology. -/
instance {α : Type} [measurable_space α] [topological_space α] [borel_space α] :
  topological_space (probability_measures α)
    := topological_space.induced (λ (μ : probability_measures α) , integrate_cont_bdd_ennval μ) infer_instance

/-- Integration of test functions against borel probability measures depends
continuously on the measure. -/
lemma integrate_cont_bdd_ennval_cont {α : Type} [measurable_space α] [topological_space α] [borel_space α] :
  continuous (@integrate_cont_bdd_ennval α _ _ _) := continuous_induced_dom

-- Remark: It felt convenient to isolate the following fact. Does it exist already?
lemma conv_seq_induced {α γ : Type*} [top_γ : topological_space γ]
  (f : α → γ) (x : ℕ → α) (x₀ : α) :
    tendsto (f ∘ x) at_top (𝓝 (f(x₀)))
      → tendsto x at_top (@nhds α (topological_space.induced f top_γ) x₀) :=
begin
  intro h_f_lim ,
  apply tendsto_nhds.mpr ,
  intros U open_U U_ni_x₀ ,
  rcases ((@is_open_induced_iff α γ top_γ U f).mp open_U) with ⟨ V , open_V , preim_V_eq_U ⟩ ,
  induction preim_V_eq_U ,
  apply tendsto_nhds.mp h_f_lim V open_V U_ni_x₀ ,
end

/-- The usual definition of weak convergence of probability measures is given in
terms of sequences of probability measures: it is the requirement that the integrals
of all continuous bounded functions against members of the sequence converge.
This characterization is shown in `weak_conv_seq_iff'` in the case when the
functions are `ennreal`-valued and the integral is `lintegral`. The most common
formulation with `ℝ`-valued functions and Bochner integrals is `weak_conv_seq_iff`. -/
theorem weak_conv_seq_iff' {α : Type*} [measurable_space α] [topological_space α] [borel_space α]
  {μseq : ℕ → probability_measures α} {μ : probability_measures α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ ∀ (f : cont_bdd_ennval α) ,
        tendsto (λ n, integrate_cont_bdd_ennval (μseq(n) : probability_measures α) f) at_top (𝓝 (integrate_cont_bdd_ennval (μ : probability_measures α) f)) :=
begin
  split ,
  { intros weak_conv ,
    have key := tendsto.comp (continuous.tendsto (@integrate_cont_bdd_ennval_cont α _ _ _) μ) weak_conv ,
    exact tendsto_pi.mp key , } ,
  { intro h_lim_forall ,
    have h_lim : tendsto (λ n, integrate_cont_bdd_ennval (μseq(n))) at_top (𝓝 (integrate_cont_bdd_ennval μ)) ,
    { exact tendsto_pi.mpr h_lim_forall , } ,
    exact conv_seq_induced _ μseq μ h_lim , } ,
end


end topology_of_weak_convergence


end portmanteau

[Kalle Kytölä]

Actually I would now really want to define both probability_measures (as suggested by Floris and done above) and finite_measures, and a coercion from the former to the latter, and equip finite Borel measures on topological spaces with the topology of weak convergence. Some parts of the weak convergence business make good sense for finite measures (and this is occasionally worthwhile, especially in view of Riesz-Markov-Kakutani). With the coercion, probability measures would "inherit" a topology from finite measures (I'd even consider defining them as a subtype).

For now, however, I had some typeclass difficulties showing that this topology is the same as the direct definition (although tidy at least claimed to prove this), so I thought I'd postpone this and go more directly along the proposal of Floris.

[Kalle Kytölä]

An alternative even simpler first code PR could be the following. The file portmanteau_topological_lemmas.lean was very short (6 tiny lemmas, less than 100 lines of actual code) and self-contained. The main question about it is probably whether something sufficiently close to these existed in already (I tried to look for versions in mathlib, of course, but also occasionally ended up including some reformulations that felt conventient for the portmanteau project). And then there will be questions about optimal implementation, golfed proofs, naming conventions, ... but perhaps they could be addressed in the PR?

So if someone with experience can tell whether (some nonempty subset of) these are PR'able (expecting improvements in the process), I could also make them my first code PR. I am almost sure some version of these lemmas would have to be used in portmanteau anyway (and likely elsewhere as well), so I don't think they would be completely useless.

[Kalle Kytölä]

I'll just copy the 6 lemmas here, perhaps that's better practice.

import tactic
import measure_theory.measurable_space
import measure_theory.borel_space


noncomputable theory
open set
open measure_theory
open measurable_space
open borel_space


namespace portmanteau

section portmanteau_topological_lemmas


variables {α : Type*} [topological_space α]


lemma meas_eq_various_of_null_bdry (μ : @measure_theory.measure α (borel α)) (E : set α) :
  (μ(frontier E) = 0) → (μ(interior E) = μ(E)) ∧ (μ(closure E) = μ(E)) :=
begin
  intro hEnullbdry ,
  have ineq_E_le_Ecl := @measure_mono α (borel(α)) μ E (closure E) subset_closure ,
  have ineq_Eint_le_E := @measure_mono α (borel(α)) μ (interior E) E interior_subset ,
  have surpr := @measure_union_le α (borel(α)) μ (interior E) (frontier E) ,
  rw ← closure_eq_interior_union_frontier at surpr ,
  simp [hEnullbdry] at surpr ,
  have mono := @measure_mono α (borel(α)) μ (interior E) (closure E) interior_subset_closure ,
  have key := le_antisymm mono surpr ,
  split ,
  { apply le_antisymm ,
    { assumption , } ,
    rw key ,
    assumption , } ,
  { apply le_antisymm ,
    { rw ← key ,
      assumption , } ,
    assumption , } ,
end


lemma open_imp_borel {γ : Type*} [top_γ : topological_space γ]
  {G : set γ} : is_open G → (borel γ).measurable_set' G
    := measurable_set_generate_from


lemma closed_imp_borel {γ : Type*} [top_γ : topological_space γ]
  {F : set γ} : is_closed F → (borel γ).measurable_set' F :=
begin
  set G := Fᶜ with hG ,
  have FeqGc := compl_compl F ,
  rw ← hG at FeqGc ,
  intro hFclosed ,
  have Gmble := open_imp_borel (is_open_compl_iff.mpr hFclosed) ,
  rw ← FeqGc ,
  exact (borel γ).measurable_set_compl G Gmble ,
end


lemma compl_frontier {γ : Type*} [topological_space γ] (A : set γ) :
  (frontier A)ᶜ = (interior A) ∪ (interior (Aᶜ)) :=
begin
  have fact := @closure_eq_compl_interior_compl γ _ Aᶜ ,
  rw compl_compl at fact ,
  suffices : frontier A = (interior A)ᶜ ∩ (interior (Aᶜ))ᶜ ,
  { rw this ,
    rw compl_inter (interior A)ᶜ (interior (Aᶜ))ᶜ ,
    repeat {rw compl_compl ,} , } ,
  rw [←frontier_compl A , ←fact] ,
  exact diff_eq (closure (Aᶜ)) (interior (Aᶜ)) ,
end


lemma interior_preimage {β γ : Type*}
  [topological_space β] [topological_space γ]
  (G : set γ) (f : β → γ) (hf : continuous f) :
    f⁻¹' (interior G) ⊆ interior (f⁻¹'(G)) :=
begin
  apply interior_maximal ,
  { have Gint_ss_G : (interior G) ⊆ G := interior_subset ,
    exact preimage_mono Gint_ss_G , } ,
  { have interior_open : is_open (interior G) := is_open_interior ,
    exact continuous_def.mp hf (interior G) interior_open , } ,
end


lemma frontier_preimage {β γ : Type*}
  [topological_space β] [topological_space γ]
  (A : set γ) (f : β → γ) (hf : continuous f) :
    frontier (f⁻¹'(A)) ⊆ f⁻¹'(frontier A) :=
begin
  apply (@compl_subset_compl β (f⁻¹'(frontier A)) (frontier (f⁻¹'(A)))).mp,
  rw [compl_frontier _ , ←preimage_compl , compl_frontier _ , preimage_union ] ,
  have one := @interior_preimage β γ _ _ A f hf ,
  have two := @interior_preimage β γ _ _ (Aᶜ) f hf ,
  exact union_subset_union one two ,
end



end portmanteau_topological_lemmas

end portmanteau

[Johan Commelin]

@Kalle Kytölä I think that it's a good exercise to PR the subset of the lemmas that isn't in mathlib yet. Unfortunately I'm not so familiar with this part of mathlib, so I can't see at a glance what that subset would be. The open_imp_borel and closed_imp_borel look like they definitely should already exist in mathlib.
The frontier_preimage seems to be missing. On the other hand, we already have

-- src/topology/basic.lean (lines 1110-1112)
lemma preimage_interior_subset_interior_preimage {f : α → β} {s : set β}
  (hf : continuous f) : f⁻¹' (interior s) ⊆ interior (f⁻¹' s) :=
interior_maximal (preimage_mono interior_subset) (is_open_interior.preimage hf)

[Kalle Kytölä]

Thank you Johan!

Indeed open_imp_borel and closed_imp_borel should probably be docs#is_open.measurable_set and docs#is_closed.measurable_set together with docs#borel_space.opens_measurable. When writing this a few months ago, I strongly suspected they exist, but I guess I wasn't good enough with the typeclasses yet to use them. With Floris' explanation of the proper way to use the typeclass docs#borel_space I think I will have more success, and these two lemmas I used are completely redundant.

Thanks for pointing out docs#preimage_interior_subset_interior_preimage --- it is the same as I wanted (and with a golfed proof). Now library_search finds it, but I think a few months ago it didn't, so maybe this is new? Anyways, makes yet another lemma above redundant!

[Kalle Kytölä]

That leaves possibly 3 lemmas above. The last two, compl_frontier and frontier_preimage, might be of general interest, so if there is not much harm PR'ing (and being ready to either improve or give up based on the PR review), I think I will do that.

The lemma meas_eq_various_of_null_bdry is probably more specific to portmanteau, but I maintain that it will be needed. I will wait a bit with it, and change the statement to use the borel_space typeclass in the way Floris explained.

[Johan Commelin]

Yes, I would PR those two lemmas. The meas_eq_various_of_null_bdry is something that I can't really comment about. I don't know enough measure theory :shrug:

[Kalle Kytölä]

Meanwhile, adding the definition of weak convergence might be a bigger thing, so I will still wait for comments to the proposal above.

At some point, if I get no drastic comments here, I will probably PR it --- and again be ready to either improve or give up based on the PR review.

But for now: comments about the proposed definition are very welcome!

[Johan Commelin]

@Kalle Kytölä I would just make the PR. I think you might get more comments/feedback there. It's good to polish stuff before you PR it, but it doesn't have to be perfect (especially for the first few PRs). There's a review process, so make use of it!

[Patrick Massot]

Give me ten minutes please.

[Patrick Massot]

In the mean time Kalle could read the style guide.

[Kalle Kytölä]

Thanks! I was anyway going to do the PR no sooner than tonight, so even more than 10 minutes is fine :smile:. But I will read the style guide before PR'ing any code.

[Patrick Massot]

Actually ten minutes were not enough and I need to run, so I'll come back later. In the mean time you can think about why borel appears in meas_eq_various_of_null_bdry. What if $\mu$ was any measure on $\alpha$?

[Kalle Kytölä]

Borel was probably an overkill assumption for the measurability of the interior, the boundary and the closure. The needed monotonicity probably holds without measurability (for the outer measure), so I guess this assumption is logically unnecessary (although in math I would only state it when I have enough measurability).

I will clean up this and others to the extent I can before PRs.

[Patrick Massot]

I'm back. Let's go through your lemmas. The first step is to remove all those spaces before commas (do they come from your native language? I know French people, including me, often put spaces before question marks and exclamation marks because that's the rule in French).

The first lemma was meas_eq_various_of_null_bdry. I already explained this morning that the borel word is useless, the lemma holds for any measure on a topological space. Let's first do a naive greedy cleanup pass. You get:

lemma meas_eq_various_of_null_bdry' [measure_space α] (μ : measure α) (E : set α)
   (hEnullbdry : μ (frontier E) = 0) : (μ (interior E) = μ E) ∧ (μ (closure E) = μ E) :=
begin
  have ineq_E_le_Ecl : μ E ≤ μ (closure E) := measure_mono subset_closure,
  have ineq_Eint_le_E : μ (interior E) ≤ μ E := measure_mono interior_subset,
  have surpr : μ (interior E ∪ frontier E) ≤ μ (interior E) + μ (frontier E) :=
    measure_union_le (interior E) (frontier E),
  rw [← closure_eq_interior_union_frontier, hEnullbdry, add_zero] at surpr,
  have key : μ (interior E) = μ (closure E) :=
    (ineq_Eint_le_E.trans ineq_E_le_Ecl).antisymm surpr,
  rw ← key at *,
  split ; { apply le_antisymm ; assumption }
end

First note how I "moved hEnullbdry left of colon". You get the exact same lemma and the proof is one line shorter without loosing any readability. Next note how I announce the inequalities in have, both increasing readability and remove any need for expliciting implicit arguments. By the way, subset_closure and interior_subset should have an explicit set argument. They are currently breaking our rules. If you're looking for a pull-request exercise you could try to fix those and see whether it uglyfies too many existing proofs. The last trick is probably using the "dot notation" for docs#has_le.le.trans and docs#has_le.le.antisymm (please ask question if you don't know this trick).

[Patrick Massot]

Now let's think about our readers. We start with three obvious inequalities with rather readable proofs. And then comes a statement labelled key and that one is obfuscated. That's mean. Let's try again.

[Patrick Massot]

lemma meas_eq_various_of_null_bdry'' [measure_space α] (μ : measure α) (E : set α)
   (hEnullbdry : μ (frontier E) = 0) : (μ (interior E) = μ E) ∧ (μ (closure E) = μ E) :=
have E_le_Ecl : μ E ≤ μ (closure E) := measure_mono subset_closure,
have Eint_le_E : μ (interior E) ≤ μ E := measure_mono interior_subset,
have key : μ (closure E) ≤ μ (interior E) := calc
  μ (closure E) = μ (interior E ∪ frontier E) : by rw closure_eq_interior_union_frontier
            ... ≤ μ (interior E) + μ (frontier E) : measure_union_le _ _
            ... = μ (interior E) : by simp [hEnullbdry],
⟨Eint_le_E.antisymm (E_le_Ecl.trans key), (key.trans Eint_le_E).antisymm E_le_Ecl⟩

Now the key step is a nice readable computation that is indeed the heart of this proof. After those three have you would expect a human reader to be convinced. In Lean there are now three possibility. The really good one is automation should take over. Unfortunately this doesn't happen here because linarith doesn't work with ennreal (ping @Rob Lewis just in case he is currently bored). The really bad one would be writing 50 lines because for some reason that obvious stuff could be Lean hard. The middle case, displayed above, is going to obfuscation mode, simply compressing the proof because it doesn't deserve space and this clearly tells the reader nothing interesting happen here.

[Patrick Massot]

A general remark. When I saw this lemma, my first reaction was: "we don't have lemmas whose conclusion is a conjunction, we split them into two lemmas, one for each conclusion". But in this case I think it's fair to keep the conjunction. The proof really gives both at the same time, I don't really see an intermediate lemma to split off, and really you want to say "those three numbers are equal" and we don't really have a nice way to say that in mathlib.

[Patrick Massot]

Let's golf the next lemma:

lemma compl_frontier {γ : Type*} [topological_space γ] (A : set γ) :
  (frontier A)ᶜ = interior A ∪ interior Aᶜ :=
begin
  -- Maybe put that in a separate lemma?
  suffices : frontier A = (interior A)ᶜ ∩ (interior (Aᶜ))ᶜ ,
  { simp [this, compl_inter] } ,
  rw [← frontier_compl, ← closure_compl],
  refl
end

[Patrick Massot]

I know parentheses are cheap, but your statement had way too many of them. It's not that hard to get used to the fact that function application has a really high priority. You could add parentheses around the final Aᶜ since the fact that complement has higher priority is much more specialized knowledge, but in that case the wrong interpretation of the formula really makes no sense at all, so there is little risk of confusion.

[Patrick Massot]

The first proof trick is you missed docs#closure_compl. The second one is using simp to get rid of complement of complement (if that is not a simp lemma then nothing is). And the last trick is refl at the end. This is a bit debatable since it relies on knowing which definition of interior we choose in mathlib, but I think that's a pretty standard choice.

[Patrick Massot]

For the last lemma, frontier_preimage, I would say your proof on paper is too complicated, but that's debatable. I would add first to mathlib:

lemma _root_.continuous.closure_preimage_subset {f : β → γ} (hf : continuous f) (A : set γ) :
  closure (f ⁻¹' A) ⊆ f ⁻¹' (closure A) :=
begin
  rw ← (is_closed_closure.preimage hf).closure_eq,
  mono*,
  exact subset_closure
end

since it seems to be missing (I included _root_ so that you can copy-paste it in your file in the middle of your portmanteau namesapce, but that wouldn't be needed in mathlib). Note how f is implicit since it can be inferred from hf, and note how this is in the continuous namespace to allow dot notation magic as in my proof of your lemma

lemma _root_.continuous.frontier_preimage_subset {f : β → γ} (hf : continuous f) (A : set γ) :
  frontier (f ⁻¹' A) ⊆ f ⁻¹' (frontier A) :=
diff_subset_diff (hf.closure_preimage_subset A) (preimage_interior_subset_interior_preimage hf)

[Patrick Massot]

Note also I think the set argument in docs#preimage_interior_subset_interior_preimage should be explicit and that lemma should be in the continuous namespace.

[Patrick Massot]

I would call it continuous.preimage_interior_subset to avoid the super long name. This is enough for autocompletion to kick off when you're looking for it.

[Patrick Massot]

That's all I have to say, I hope you'll pick up some tricks!

[Mario Carneiro]

Patrick Massot said:

A general remark. When I saw this lemma, my first reaction was: "we don't have lemmas whose conclusion is a conjunction, we split them into two lemmas, one for each conclusion". But in this case I think it's fair to keep the conjunction. The proof really gives both at the same time, I don't really see an intermediate lemma to split off, and really you want to say "those three numbers are equal" and we don't really have a nice way to say that in mathlib.

When the proof proves both parts at the same time, you should first prove the conjunction as a lemma and then immediately split off the conjuncts as corollaries. In this case the lemma could instead be key though, your choice

[Kalle Kytölä]

Thank you @Patrick Massot for thorough explanations!

Many of the principles above are very clear. I hopefully pick up those and some of the tricks from your explanation. Other parts of your advice will surely require more practice for me to truly internalize (including efficient use of dot notation, term proofs, etc.), but I think I am getting at least steps to the right direction from here.

Style (including everything from spaces before commas to naming conventions and arguments before colon etc.) is something I had completely disregarded while writing the first sorry-free project. I naturally intend to stick to style guidelines of the mathlib the best I can when actually starting to make PRs (hopefully with the aid of this Zulip and the review process). I will in particular still look at the style guide; so far I only had time to glance through it. Sorry that some style issues created additional work for the helpful reviewers here when transitioning from my experimentation to something PRable! I could (and perhaps should?) have made some more effort in that direction at an earlier stage, but above I really primarily intended to identify the pieces with which I'd start the practice towards useful contributing.

The situation with the right generality of assumptions (and even statements) was similar. I so far settled for whatever sufficed for this project. Again for any parts I might PR to mathlib, I'd of course strive for the good generality (first by my own best effort, and then hopefully with the help of experienced reviewers). In many cases I actually expect instead to find that the statements I made have an existing better implementation in mathlib (this turned out to be the case e.g. with open_imp_borel and closed_imp_borel above), so in those cases my goal is rather to learn to use mathlib better. Only with actually missing stuff I'd start to optimize the generality and implementation.

I highly appreciate both your general thoughtful approach and carefully justified specific judgements, e.g., regarding what the reader might want to see in a proof. In the back of my mind I think I expected mathlib-quality with lemmas such as these to mainly mean having the statements readable, general, and well implemented, but proofs golfed to some obfuscated form optimized for length and efficiency only.

Anyway, with the above comments in mind I hope to get to making some small PRs in the near future!

[Kalle Kytölä]

(deleted)

[Kalle Kytölä]

Ok, so I'm closer to getting started with some tiny PRs, I hope. I think I will split to even smaller pieces. I'd just like to make sure of a few last things before making the PRs.

[Kalle Kytölä]

I like Patrick's suggestion of separating even a substatement (frontier_eq_inter_compl_interior below) to another small lemma, since it essentially doesn't add to the length and it could be useful again (it will used once right away with the original lemma, now compl_frontier_eq_union_interior below). I think these don't belong to portmanteau namespace, though, and I would be happy to avoid creating a new file in this first PR of any code. Does it make sense to PR these to topology/basic.lean, towards the end of the segment dealing with frontier (say after docs#closure_eq_self_union_frontier)?

My current proposal of the code to PR is:

lemma frontier_eq_inter_compl_interior {γ : Type*} [topological_space γ] (A : set γ) :
  frontier A = (interior A)ᶜ ∩ (interior (Aᶜ))ᶜ :=
by { rw [←frontier_compl, ←closure_compl], refl }

lemma compl_frontier_eq_union_interior {γ : Type*} [topological_space γ] (A : set γ) :
  (frontier A)ᶜ = interior A ∪ interior Aᶜ :=
begin
  rw frontier_eq_inter_compl_interior A,
  simp only [compl_inter, compl_compl],
end

[Kalle Kytölä]

Also another suggestion by Patrick included adding a new lemma, this time to the continuous namespace (via _root_ in Patrick's code and below). I again think these wouldn't belong to portmanteau, they are generalities.

@Patrick Massot, if you don't want to PR these two (the code below is from your message above, except for the introductions of the variables), I could also do that. In that case, is topology/basic.lean again appropriate, in the segments about closure and frontier? Would I be right to separate this from the PR above? (Are these becoming too microscopic?)

lemma _root_.continuous.closure_preimage_subset {β γ : Type*}
  [topological_space β] [topological_space γ] {f : β → γ} (hf : continuous f) (A : set γ) :
  closure (f ⁻¹' A) ⊆ f ⁻¹' (closure A) :=
begin
  rw ← (is_closed_closure.preimage hf).closure_eq,
  mono*,
  exact subset_closure
end

lemma _root_.continuous.frontier_preimage_subset {β γ : Type*}
  [topological_space β] [topological_space γ] {f : β → γ} (hf : continuous f) (A : set γ) :
  frontier (f ⁻¹' A) ⊆ f ⁻¹' (frontier A) :=
diff_subset_diff (hf.closure_preimage_subset A) (preimage_interior_subset_interior_preimage hf)

[Kalle Kytölä]

With meas_eq_various_of_null_bdry I'd perhaps wait a bit until I get to the level of PRing that I dare create new files --- this one might be natural in the portmanteau namespace. (Or is there a natural place for this elsewhere?)

[Patrick Massot]

Those four lemmas should indeed go into topology.basic, in a single PR. The last one is trickier to locate but I guess could go close to the definition of borel. It doesn't need borel but this is where people would probably expect to see it. I don't mind PRing those lemmas myself, but if you want an exercise in PRing then it should be perfect.

[Kalle Kytölä]

Ok, then I'd like to take these as an exercise and make the PR.

Thank you very much for the help, all! As a punishment "reward", I will request PR reviews from those who helped me out here. (Really I want to make sure that I didn't in the end go too much against your good advice.) I trust you know how to say no to that, if you don't feel like looking at these any further :smile:.

[Kalle Kytölä]

If all goes well with these PR exercises, I will probably follow up with some new PRs of the portmanteau content. The reviewers can send me back to the drawing board (and to this Zulip) whenever appropriate! I will of course try to first polish the contents myself, and in particular follow the style guide.