More theorems!! integral less than equal integral ?

Stream: new members

[Arshak Parsa]

I came back with more theorems! :)
Are any of these theorems provable?

import Mathlib

open MeasureTheory Topology ProbabilityTheory

lemma integral_le_integral (f : ℝ → ℝ) (g : ℝ → ℝ) (hpf : ∀x, 0 ≤ f x) (hle : ∀x, g x ≤ f x) (hi : Integrable f) : ∫ (x : ℝ), g x ≤ ∫ (x : ℝ), f x := by
  sorry

lemma Integrable.forall_le_integrable (f : ℝ → ℝ) (g : ℝ → ℝ) (hle : ∀x, g x ≤ f x) (hi : Integrable f) : Integrable g := by
  sorry

lemma HasFiniteIntegral.indicator (f : ℝ → ℝ) (E : Set ℝ) (hfin : Integrable f) : HasFiniteIntegral (E.indicator f) := by
  -- I need the above theorems to prove this
  rw [Integrable] at hfin
  rw [HasFiniteIntegral]
  sorry

this might be helpful. (btw I don't understand it and it has an extra assumption integral f =0 )

[Luigi Massacci]

@loogle integral_mono

[loogle]

:exclamation: unknown identifier 'integral_mono'
Did you mean "integral_mono", MeasureTheory.integral_mono, or something else?

[Luigi Massacci]

For the first one you definitely need to add an hypothesis that g is integrable, unless you meant the positivity hypothesis for g instead of f (then it should work)

[Luigi Massacci]

The second one is not true, just take $g \equiv -1$ and $f$ you favourite positive integrable function

[Luigi Massacci]

For no.3, @loogle “integrable_indicator”

[Luigi Massacci]

@loogle integrable_indicator

[loogle]

:exclamation: <input>:1:0: expected end of input

[Henrik Böving]

@loogle "integrable_indicator"

[loogle]

:search: MeasureTheory.IntegrableOn.integrable_indicator, MeasureTheory.integrable_indicator_iff, and 1 more

[Luigi Massacci]

@loogle integrable_indicator

[loogle]

:exclamation: unknown identifier 'integrable_indicator'
Did you mean "integrable_indicator" or MeasureTheory.IntegrableOn.integrable_indicator?

[Arshak Parsa]

integrable_indicator requires the assumption of measurablity. I don't see why it needs that. If the integral of f over R is finite, then how could the integral of E.indicator f become infinite? (Assume f is positive everywhere)

[Arshak Parsa]

Also, g is positive, too (Sorry, I forgot to mention)
Actually, I want to replace g with E.indicator f to prove the third one

[Arshak Parsa]

I also managed to prove a lintegral version of the first one :

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 * ℙ {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

I'm still trying to use this theorem to prove integral_le_integral...

[Arshak Parsa]

I modified the first one, (f is also possitive and it is a probability density function in fact!)

lemma integral_le_integral (f : ℝ → ℝ) (g : ℝ → ℝ) (hpg : ∀x, 0 ≤ g x) (hle : ∀x, g x ≤ f x) (hi : Integrable f) : ∫ (x : ℝ), g x ≤ ∫ (x : ℝ), f x := by
  sorry

[Etienne Marion]

docs#MeasureTheory.integral_mono_of_nonneg

[Etienne Marion]

docs#Set.indicator_le'