is_open_pos_measure

Stream: maths

[David Loeffler]

I found myself needing to show that the restriction of the usual measure on ℝ to the interval Ioc 0 (2 * π) satisfies is_open_pos_measure, i.e. nonempty open sets have non-zero measure. This sounds like it should be a triviality, but I couldn't find a slick proof in the case at hand -- I ended up with the 22-line monstrosity below. Can anyone suggest a more civilized approach?

This was my code:

lemma silly_lemma : is_open_pos_measure (volume : measure (Ioc 0 (2 * π))) :=
begin
  split, intros V hV1 hV2,
  rw ←volume_image_subtype_coe, swap, exact measurable_set_Ioc,
  refine (measure_pos_of_nonempty_interior _ _).ne',
  rw is_open_induced_iff at hV1,
  rcases hV1 with ⟨W, ⟨hW1, hW2⟩⟩,
  rw [←hW2, subtype.image_preimage_coe, interior_inter, interior_Ioc, interior_eq_iff_open.mpr hW1],
  have : (W ∩ Ioc 0 (2 * π)).nonempty,
  { rwa [←subtype.image_preimage_coe, hW2, nonempty_image_iff] },
  rcases this with ⟨x, ⟨hx1, hx2⟩⟩,
  rcases ne_or_eq x (2 * π) with h|h,
  { -- some x ≠ 2 * π is in W
    exact ⟨x, ⟨hx1, ⟨hx2.1, lt_of_le_of_ne hx2.2 h⟩⟩⟩ },
  { -- 2 * π is in W
    rw metric.is_open_iff at hW1,
    specialize hW1 x hx1, rw h at hW1,
    rcases hW1 with ⟨ε, ⟨hε1, hε2⟩⟩,
    use max π (2 * π - ε / 2),
    split,
    { apply hε2, rw ball_eq_Ioo, split,
      { refine lt_of_lt_of_le _ (le_max_right _ _), linarith },
      { apply max_lt, linarith [pi_pos], linarith }, },
    { split,
      { exact lt_of_lt_of_le pi_pos (le_max_left _ _) },
      { apply max_lt, linarith [pi_pos], linarith, } } },
end

[Eric Rodriguez]

can you give us a mwe with the imports+open statements and such?

[David Loeffler]

OK, I've made it a self-contained MWE

[Eric Rodriguez]

coe here is an open map, right?

[Eric Rodriguez]

my point is, I haven't used this area too much but I do wonder whether this is more palatable:

import analysis.special_functions.integrals

noncomputable theory
open_locale real
open real measure_theory measure_theory.measure set

lemma set.nonempty.subset {α} {s t : set α} (hs : s.nonempty) (h : s ⊆ t) : t.nonempty :=
Exists.imp h hs

lemma silly_lemma : is_open_pos_measure (volume : measure (Ioc 0 (2 * π))) :=
begin

  refine ⟨λ V hV1 hV2, _⟩,
  rw ←volume_image_subtype_coe (measurable_set_Ioc : measurable_set (Ioc (0 : ℝ) _)),
  refine (measure_pos_of_nonempty_interior _ _).ne',
  apply set.nonempty.subset,
  swap 2, apply is_open_map.image_interior_subset,
  sorry, /- `coe` is open -/
  rw nonempty_image_iff,
end

[David Loeffler]

No, it isn't, that's the point: it's the inclusion of an Ioc interval which is not an open set, so the inclusion is a continuous map but not an open one.

[Eric Rodriguez]

oh, it's an Ioc :/ my mind guessed it was an Ioo, drats

[Eric Rodriguez]

I mean, I guess in the end that's the proof I'd expect to give in that case. Maybe it's just worth generalising this to all Iocs and open sets, hopefully then order_duel gives it for free for Icos, and then no-one has to worry about this again