integral_union without measurable assumption

Stream: new members

[Arshak Parsa]

Is it possible to prove this theorem without the assumption of MeasurableSet ?
If it is not possible then could you give me a counterexample ?

import Mathlib

open MeasureTheory Topology ProbabilityTheory

theorem Integrable.integral_union {f : ℝ → ℝ} (A B : Set ℝ) (hd : Disjoint A B) (hi : Integrable f)
  (hp : f ≥ 0) (hu : ∫ (x : ℝ), f x = 1) :
    ∫ (x : ℝ) in A ∪ B, f x = (∫ (x : ℝ) in A, f x) + ∫ (x : ℝ) in B, f x := by
  -- I don't want to assume A or B are measurableSet
  -- I can't use integral_union because it assumes B is measurable
  sorry

[Arshak Parsa]

I don't want to add the assumption of MeasurableSet everywhere :/

[Kevin Buzzard]

I don't know for sure because this is way out of my comfort zone, but if A and B are not measurable then I'm guessing that lean defines the integral to be zero -- I might be wrong about this, maybe it's some inner or outer measure -- but either way if also A union B is actually measurable then I suspect the result might be false in this case. Sorry if I'm talking nonsense

[Sébastien Gouëzel]

You need to assume that A or Bis measurable, otherwise it's just wrong.

[Philippe Duchon]

Doen't it actually need both A and B to be measurable? If the integral is defined to be zero on a non-measurable set and only one of A and B is measurable, the equality won't hold unless the integral on the measurable part is zero.

[Arshak Parsa]

Actually, there is a theorem in mathlib that requires only one of them to be measurable.
But my integral is integrable anywhere, I thought it might help :/

[Kevin Buzzard]

The constant function 1 is integrable but you still can't assign a sensible meaning to its integral over a non-measurable set.

[Arshak Parsa]

I think I need to add the assumption that at least one of these integrals is non zero

[Filippo A. E. Nuccio]

And why are assuming hu at any rate?

[Arshak Parsa]

@Filippo A. E. Nuccio
I am working with probability density functions, so I added that in case it might be useful

[Filippo A. E. Nuccio]

Well, I would say that this is a bit strange. With the right assumptions (measurability of A or B) the theorem is true without hu, and without these assumptions it is false even assuming hu. Of course you are free to add whatever assumptions you like, but to me is like assuming that f is $C^\infty$ " just in case it helps".

[Sébastien Gouëzel]

The integral is not defined to be 0 on a non-measurable set, it is defined to be the integral with respect to \mu.restrict A, which makes sense for any A but is not really what you expect when A is not measurable (you get the same as the restriction of mu to the measurable hull of A, which is a "smallest" measurable set containing A).

[Sébastien Gouëzel]

If A is disjoint from B and neither of them are measurable, then their measurable hulls could both well be the whole space, and you would get ∫ (x : ℝ) in A, f x = ∫ (x : ℝ) in B, f x = ∫ f x = 1, which explains why your theorem is wrong. On the other hand, if B is measurable, then its complement is also measurable. As it contains A, it also contains the measurable hull of A, so the measurable hull of A is disjoint from B and everything is fine.

[Arshak Parsa]

@Sébastien Gouëzel
How can A and B be disjoint, and their measurable hulls be the whole space?

[Etienne Marion]

If the sigma algebra is just the empty set and the whole set for instance

[Arshak Parsa]

if measurable hull of A is the whole space, then A must be the whole space.

[Arshak Parsa]

The measurable space here is Real.measurableSpace, which is borel ℝ.
(Does it help?)

[Arshak Parsa]

The only case in which A is not measurable is when it is neither open nor closed

[Sébastien Gouëzel]

Non-measurable sets can be very weird, much more than you expect!

[Arshak Parsa]

I didn't need to add measurable assumptions when I was working with tsum. I don't know why integral wants the measurable assumption :/

[Arshak Parsa]

(tsum_union_disjoint doesn't require measurablity assumptions)

[Kevin Buzzard]

But it does require summability assumptions, which are the analogue in that situation (that's a lemma about topology, not measure theory). As has been explained already, the integral lemma wants the measurable assumptions because the result is false without it.

[Arshak Parsa]

Ok, I give up. I guess it's impossible without the measurableSet assumption. I resolve this thread. I found this, which says it is impossible to construct a non measurable set in R but the existence can be proven with AC. (I also managed to avoid proving this theorem by adding QuasiDistFunc to my project, so I relaxed the third axiom of Kolmogorov)

[Notification Bot]

Arshak Parsa has marked this topic as resolved.

[Luigi Massacci]

lean's mathematical library very much depends on AC, you are unfortunately(?) not working with Solovay's model here

[Luigi Massacci]

Unrelatedly: don't feel like you need to close threads, in fact it's encouraged not to do it since it breaks links

[Notification Bot]

Arshak Parsa has marked this topic as unresolved.

[Arshak Parsa]

I managed to prove an indicator version of this theorem :

import Mathlib

open MeasureTheory Topology ProbabilityTheory Filter Set

lemma lintegral_le_lintegral {f g : ℝ → ℝ} (hle : ∀x, g x ≤ f x) (hi : Integrable f) : ∫⁻  (x : ℝ), ENNReal.ofReal (g x) ≤ ∫⁻ (x : ℝ), ENNReal.ofReal (f x)  := by
  set f' : ℝ → ENNReal := fun r => ENNReal.ofReal (f r)
  set g' : ℝ → ENNReal := fun r => ENNReal.ofReal (g r)
  have hle' : ∀x, g' x ≤ f' x := by exact fun x ↦ ENNReal.ofReal_le_ofReal (hle x)
  have hae' : g' ≤ᶠ[ae volume] f' := by
    rw [EventuallyLE.eq_1]
    exact ae_of_all volume hle'
  have hm : AEMeasurable f := by exact Integrable.aemeasurable hi
  have hm' : AEMeasurable f' := by exact AEMeasurable.ennreal_ofReal hm
  calc
    (∫⁻  (x : ℝ), g' x) ≤ (∫⁻ (a : ℝ), g' a) + 1 * volume {x | g' x + 1 ≤ f' x} := by exact le_self_add
    _ ≤ (∫⁻  (x : ℝ), f' x) := by exact lintegral_add_mul_meas_add_le_le_lintegral hae' hm' 1

lemma HasFiniteIntegral_indicator {f : ℝ → ℝ} (hp : ∀x, 0 ≤ f x) (hi : Integrable f) (E : Set ℝ) : HasFiniteIntegral (E.indicator f) := by
  rw [HasFiniteIntegral]
  have hp2 (x : ℝ) : (E.indicator f) x ≤ f x := by
    rw [indicator]
    by_cases h : x ∈ E
    · aesop
    · simp [h, hp]
  have hfin : (∫⁻ (x : ℝ), ENNReal.ofReal (E.indicator f x)) < ⊤ := by
    calc
      (∫⁻ (x : ℝ), ENNReal.ofReal (E.indicator f x)) ≤ ∫⁻ (x : ℝ), ENNReal.ofReal (f x) := by exact lintegral_le_lintegral hp2 hi
      _ < ⊤ := by exact Integrable.lintegral_lt_top hi
  have hfin2 : (∫⁻ (x : ℝ), ENNReal.ofReal (E.indicator f x)) ≠ ⊤ := by aesop
  have hle (x : ℝ) : 0 ≤ (E.indicator f) x := by exact indicator_nonneg (fun a _ ↦ hp a) x
  have := hasFiniteIntegral_toReal_of_lintegral_ne_top hfin2
  simp_rw [ENNReal.toReal_ofReal (hle _)] at this
  exact this

lemma Integrable.indicator {f : ℝ → ℝ} (E : Set ℝ) (hnz : ∫ (x : ℝ), (E.indicator f) x ≠ 0)
  (hp : ∀x, 0 ≤ f x ) (hi : Integrable f):
      Integrable (E.indicator f) := by
  rw [Integrable]
  constructor
  · exact not_imp_comm.1 integral_non_aestronglyMeasurable hnz
  · exact HasFiniteIntegral_indicator hp hi E

-- this is the main result :)
theorem integral_indicator_union {f : ℝ → ℝ} (A B : Set ℝ) (hd : Disjoint A B) (hi : Integrable f)
  (hnzA : ∫ (x : ℝ) , A.indicator f x ≠ 0) -- I added these two assumptions
  (hnzB : ∫ (x : ℝ) , B.indicator f x ≠ 0) -- but I feel they can be removed
  (hp : ∀x, 0 ≤ f x ) :
    ∫ (x : ℝ) , (A ∪ B).indicator f x = (∫ (x : ℝ) , A.indicator f x) + ∫ (x : ℝ) , B.indicator f x := by
  -- no MeasurableSet
  simp_rw [indicator_union_of_disjoint hd f]
  rw [integral_add]
  exact Integrable.indicator A hnzA hp hi
  exact Integrable.indicator B hnzB hp hi

#print axioms integral_indicator_union

I had to add two extra assumptions, but I don't think they are necessary .

[Arshak Parsa]

No measurability assumptions!

[Arshak Parsa]

But, still I can't write it in ∫ (x : ℝ) in A, f x because integral_indicator requires measurability :/
Anyways I changed the definition of continuous distribution function in my project...

[Sébastien Gouëzel]

Your assumption hnzA says that the function A.indicator f is measurable, as the integral of non-measurable functions is zero by definition. So in fact you are assuming measurability.

[Arshak Parsa]

Sébastien Gouëzel said:

The integral is not defined to be 0 on a non-measurable set, it is defined to be the integral with respect to \mu.restrict A, which makes sense for any A but is not really what you expect when A is not measurable (you get the same as the restriction of mu to the measurable hull of A, which is a "smallest" measurable set containing A).

But you mentioned that it is not defined to be zero if I have understood correctly :thinking:

[Etienne Marion]

No, the integral over a set is defined as the integral against the restriction of the measure to the corresponding set. But the integral of a non measurable function is defined to be 0, these are different things.

[Etienne Marion]

Which also explains why docs#MeasureTheory.integral_indicator requires measurability.

[Etienne Marion]

Out of curiosity, why do you wish to get rid of measurability assumptions?

[Arshak Parsa]

The book I'm formalizing doesn't use measure theory, and I want the theorems to be similar as their latex version

[Arshak Parsa]

The integral in the book is probably the reimann integral, but the integral in lean is a bochner integral

[Etienne Marion]

But maybe measurability assumptions are hidden by topological ones. You might be able not to mention measurability in assumptions and only use it inside the proofs (unless you do not want measurability to appear anywhere)

[Arshak Parsa]

I think adding the hnzA is better than saying it is measurable.

[Arshak Parsa]

But it is weird. If we can't construct a non measurable set in R, then how it can exist :|

[Etienne Marion]

That’s a deep question :sweat_smile:

[Kevin Buzzard]

Sure we can construct one: we can show that the set of nonmeasurable sets is nonempty and then choose one using the axiom of choice.

[Ruben Van de Velde]

Depends on what you mean by "construct"

[Ruben Van de Velde]

In this thread, it was a reference to this constructivist answer to https://math.stackexchange.com/questions/226559/examples-of-non-measurable-sets-in-mathbbr