diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet.lean new file mode 100644 index 00000000..039a2cbb --- /dev/null +++ b/LMLExplore/EValues/EffectiveSet.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Statlib.EValues.RIPr +public import LMLExplore.MeasureTheory.Integral.Lebesgue.Add + +/-! +# The effective null + +The effective null of a null hypothesis `S : Set (Measure Ω)` is Statlib's `effectiveSet S`: the +measures `μ` under which every e-variable `X` for `S` has `∫⁻ X ∂μ ≤ 1`. It is the set over which +Statlib's duality `maxUtility_eq_iInf_klIntegral_effectiveSet` minimizes, and it describes the +alternatives that a null can be tested against: e-variables cannot distinguish `S` from its +effective null, and, when `S` consists of probability measures, every measure outside its +effective null is detected by a level-`α` test. + +This file proves the structural properties of the effective null on any measurable space, with no +dominating measure and no convexity. Unless stated otherwise below, the results hold for any set of +measures `S`. + +## Main statements + +* `ProbabilityTheory.subset_effectiveSet_iff`: `S ⊆ effectiveSet S` exactly when every member of + `S` has mass at most `1`. +* `ProbabilityTheory.comp_mem_effectiveSet`: the effective null contains every mixture `κ ∘ₘ π` of + members of the effective null over a measure `π` of mass at most `1`, in particular, for a null + of measures of mass at most `1`, every mixture of members of `S` over a probability measure. +* `ProbabilityTheory.convex_effectiveSet`, `ProbabilityTheory.convexHull_subset_effectiveSet`: the + effective null is convex, and, for a null of measures of mass at most `1`, contains the convex + hull of `S`. +* `ProbabilityTheory.isLowerSet_effectiveSet`: the effective null is solid. +* `ProbabilityTheory.mem_effectiveSet_of_measure_le_liminf`, + `ProbabilityTheory.mem_effectiveSet_of_tendsto`: the effective null is closed under setwise + convergence, along any filter, and more generally contains every measure `μ` with + `μ s ≤ liminf (μs · s)` for every measurable `s`, for a net `μs` eventually in it. +* `ProbabilityTheory.isEVar_effectiveSet_inter_iff`: for a null `S` of probability measures, `S` + and the probability measures of its effective null have the same e-variables, and hence + (`ProbabilityTheory.effectiveSet_effectiveSet_inter`) the same effective null. +* `ProbabilityTheory.absolutelyContinuous_of_mem_effectiveSet`: if every member of `S` is + absolutely continuous with respect to `μ`, so is every member of the effective null. +* `ProbabilityTheory.exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet`: a measure outside the + effective null of `S` is detected by a bounded e-variable. +* `ProbabilityTheory.exists_powered_test_iff`: for a null `S` of probability measures, + a measure `Q` admits, for some `α ∈ (0, 1)`, a level-`α` test for `S` with power larger than `α` + under `Q` exactly when `Q` is not in the effective null of `S` [RW, Theorem 6.10]. + +## References + +* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information + projection*, Ann. Statist. 53 (2025), arXiv:2402.18810, Definition 3.1 and Lemma 4.5. +* [RW] A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in + Statistics 1 (2025), arXiv:2410.23614v6, Fact 3.6, §6.3.1 and Theorem 6.10. +-/ + +public section + +open MeasureTheory Filter Set + +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S T : Set (Measure Ω)} {μ ν Q : Measure Ω} + +/-- The effective null is monotone in the null. -/ +@[gcongr] +theorem effectiveSet_mono (hST : S ⊆ T) : effectiveSet S ⊆ effectiveSet T := + fun _ hμ X hX ↦ hμ X (hX.anti_set hST) + +/-- A null is contained in its effective null exactly when each of its members has mass at +most `1`; in particular a null of probability measures is contained in its effective null. -/ +theorem subset_effectiveSet_iff : S ⊆ effectiveSet S ↔ ∀ P ∈ S, P univ ≤ 1 := + ⟨fun h _ hP ↦ measure_univ_le_one_of_mem_effectiveSet (h hP), + fun hS P hP _ hX ↦ (hX.lintegral_le_measure_univ P hP).trans (hS P hP)⟩ + +/-- A null of measures of mass at most `1` is contained in its effective null. -/ +theorem subset_effectiveSet (hS : ∀ P ∈ S, P univ ≤ 1) : S ⊆ effectiveSet S := + subset_effectiveSet_iff.mpr hS + +/-- The effective null contains every mixture `κ ∘ₘ π` over a measure `π` of mass at most `1` of +a kernel `κ` whose values are `π`-almost surely in the effective null. With +`subset_effectiveSet`, this contains every mixture over a probability measure of a kernel with +values in a null of probability measures [LRR25, Definition 3.1]. -/ +theorem comp_mem_effectiveSet {Θ : Type*} {mΘ : MeasurableSpace Θ} {π : Measure Θ} + {κ : Kernel Θ Ω} (hπ : π univ ≤ 1) (hκ : ∀ᵐ θ ∂π, κ θ ∈ effectiveSet S) : + κ ∘ₘ π ∈ effectiveSet S := by + intro X hX + rw [Measure.lintegral_bind κ.aemeasurable hX.measurable.aemeasurable] + calc ∫⁻ θ, ∫⁻ ω, X ω ∂κ θ ∂π + _ ≤ ∫⁻ _, 1 ∂π := lintegral_mono_ae (hκ.mono fun θ hθ ↦ hθ X hX) + _ ≤ 1 := by simpa using hπ + +/-- The effective null is convex. -/ +theorem convex_effectiveSet : Convex ℝ≥0∞ (effectiveSet S) := by + intro μ hμ ν hν a b _ _ hab + -- A convex combination is a mixture over the two-point space `Bool`. + have h_eq : Kernel.boolKernel μ ν ∘ₘ (a • Measure.dirac false + b • Measure.dirac true) = + a • μ + b • ν := by + simp [Measure.comp_add, Measure.comp_smul, Measure.dirac_bind (Kernel.measurable _)] + rw [← h_eq] + refine comp_mem_effectiveSet (by simp [hab]) (.of_forall fun x ↦ ?_) + cases x <;> simpa + +/-- The effective null of a null of measures of mass at most `1` contains its convex hull. -/ +theorem convexHull_subset_effectiveSet (hS : ∀ P ∈ S, P univ ≤ 1) : + convexHull ℝ≥0∞ S ⊆ effectiveSet S := + convexHull_min (subset_effectiveSet hS) convex_effectiveSet + +/-- The effective null is solid: a measure below a member of the effective null is a member. -/ +theorem isLowerSet_effectiveSet : IsLowerSet (effectiveSet S) := + fun _ _ hμν hν X hX ↦ (lintegral_mono' hμν le_rfl).trans (hν X hX) + +/-- A measure below a member of the effective null is a member of the effective null. -/ +theorem mem_effectiveSet_of_le (hν : ν ∈ effectiveSet S) (hμν : μ ≤ ν) : μ ∈ effectiveSet S := + isLowerSet_effectiveSet hμν hν + +/-- If `μs i` is eventually in the effective null along a filter, and `μ s` is at most the limit +inferior of `μs i s` for every measurable set `s`, then `μ` is in the effective null. -/ +theorem mem_effectiveSet_of_measure_le_liminf {ι : Type*} {l : Filter ι} [l.NeBot] + {μs : ι → Measure Ω} (hμs : ∀ᶠ i in l, μs i ∈ effectiveSet S) + (h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l) : + μ ∈ effectiveSet S := fun X hX ↦ + (lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure hX.measurable + h).trans (liminf_le_of_frequently_le (hμs.mono fun _ hi ↦ hi X hX).frequently) + +/-- The effective null is closed under setwise convergence: if `μs i s` tends to `μ s` along a +filter for every measurable set `s`, and `μs i` is eventually in the effective null, then so is +`μ`. The filter is arbitrary, so that the effective null is closed for the topology of setwise +convergence and not only sequentially closed. -/ +theorem mem_effectiveSet_of_tendsto {ι : Type*} {l : Filter ι} [l.NeBot] {μs : ι → Measure Ω} + (hμs : ∀ᶠ i in l, μs i ∈ effectiveSet S) + (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : + μ ∈ effectiveSet S := + mem_effectiveSet_of_measure_le_liminf hμs fun s hs ↦ (h s hs).liminf_eq.ge + +/-- A measurable set that is null for every member of `S` is null for every member of the +effective null of `S`. -/ +theorem measure_eq_zero_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S) {s : Set Ω} + (hs : MeasurableSet s) (hS : ∀ P ∈ S, P s = 0) : μ s = 0 := by + classical + -- The function equal to `∞` on `s` and to `1` elsewhere is an e-variable for `S`. + have hX : IsEVar (s.piecewise (fun _ ↦ ∞) 1) S := + (isEVar_one S).congr (measurable_const.piecewise hs measurable_const) fun P hP ↦ by + filter_upwards [measure_eq_zero_iff_ae_notMem.mp (hS P hP)] with ω hω + simp [hω] + have h : ∞ * μ s ≤ 1 := by + rw [← lintegral_indicator_const hs] + refine (lintegral_mono fun ω ↦ ?_).trans (hμ _ hX) + by_cases hω : ω ∈ s <;> simp [hω] + by_contra h_ne + simp [ENNReal.top_mul h_ne] at h + +/-- If every member of `S` is absolutely continuous with respect to a measure `ν`, so is every +member of the effective null of `S`. -/ +theorem absolutelyContinuous_of_mem_effectiveSet (hμ : μ ∈ effectiveSet S) + (hS : ∀ P ∈ S, P ≪ ν) : μ ≪ ν := by + refine Measure.AbsolutelyContinuous.mk fun s hs hνs ↦ ?_ + exact measure_eq_zero_of_mem_effectiveSet hμ hs fun P hP ↦ hS P hP hνs + +/-- An e-variable for `S` is an e-variable for the probability measures of the effective null of +`S`. -/ +theorem IsEVar.effectiveSet_inter {X : Ω → ℝ≥0∞} (hX : IsEVar X S) : + IsEVar X (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) := + .of_lintegral_le_one (S := effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) (fun _ hμ ↦ hμ.2) + hX.measurable fun _ hμ ↦ hμ.1 X hX + +/-- A null of probability measures and the probability measures of its effective null have the +same e-variables. -/ +theorem isEVar_effectiveSet_inter_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) {X : Ω → ℝ≥0∞} : + IsEVar X (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) ↔ IsEVar X S := by + refine ⟨fun hX ↦ hX.anti_set fun P hP ↦ ?_, IsEVar.effectiveSet_inter⟩ + exact ⟨subset_effectiveSet (fun P hP ↦ (hS P hP).measure_univ.le) hP, hS P hP⟩ + +/-- A null of probability measures and the probability measures of its effective null have the +same effective null. -/ +theorem effectiveSet_effectiveSet_inter (hS : ∀ P ∈ S, IsProbabilityMeasure P) : + effectiveSet (effectiveSet S ∩ {μ | IsProbabilityMeasure μ}) = effectiveSet S := by + ext μ + simp only [mem_effectiveSet_iff, isEVar_effectiveSet_inter_iff hS] + +/-- The truncation `min X c` of an e-variable `X` for `S` at a level `c ≥ 1` is an e-variable for +`S`. -/ +theorem IsEVar.min_const {X : Ω → ℝ≥0∞} (hX : IsEVar X S) {c : ℝ≥0∞} (hc : 1 ≤ c) : + IsEVar (fun ω ↦ min (X ω) c) S where + measurable := hX.measurable.min measurable_const + eintegral_ne_bot P hP := by + -- The negative part of `y - 1` is `1 - y`, and `1 - min y c = 1 - y` since `1 ≤ c`, so + -- `min X c - 1` has the same negative part as `X - 1`. + have h_neg (y : ℝ≥0∞) : (-((y : EReal) - 1)).toENNReal = 1 - y := by + simpa [EReal.toENNReal_sub, EReal.coe_ennreal_nonneg] using + congrArg EReal.toENNReal (EReal.neg_coe_ennreal_sub (u := y) (.inr ENNReal.one_ne_top)) + have h_min (y : ℝ≥0∞) : 1 - min y c = 1 - y := by + rcases le_total y c with h | h + · simp [h] + · simp [h, tsub_eq_zero_of_le hc, tsub_eq_zero_of_le (hc.trans h)] + simpa [eintegral_ne_bot_iff_lintegral_ne_top, h_neg, h_min] using hX.eintegral_ne_bot P hP + eintegral_nonpos P hP := (eintegral_mono fun ω ↦ + EReal.sub_le_sub (mod_cast min_le_left _ _) le_rfl).trans (hX.eintegral_nonpos P hP) + +/-- A measure `Q` outside the effective null of a null `S` is detected by a +bounded e-variable: some e-variable for `S` bounded by an integer `N ≥ 2` has expectation larger +than `1` under `Q`. -/ +theorem exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet (hQ : Q ∉ effectiveSet S) : + ∃ Y : Ω → ℝ≥0∞, ∃ N : ℕ, 2 ≤ N ∧ IsEVar Y S ∧ (∀ ω, Y ω ≤ N) ∧ 1 < ∫⁻ ω, Y ω ∂Q := by + obtain ⟨X, hX, hXQ⟩ : ∃ X, IsEVar X S ∧ 1 < ∫⁻ ω, X ω ∂Q := by + simpa [mem_effectiveSet_iff] using hQ + -- `Y` is the truncation `min X N` of an e-variable `X` with expectation larger than `1` under + -- `Q`, for `N` large enough. By monotone convergence, the truncations `min X N` have + -- expectation larger than `1` under `Q` from some level `N ≥ 2` on. + have hXm := hX.measurable + have h_tendsto : Tendsto (fun N : ℕ ↦ ∫⁻ ω, min (X ω) N ∂Q) atTop (𝓝 (∫⁻ ω, X ω ∂Q)) := by + refine lintegral_tendsto_of_tendsto_of_monotone (fun N ↦ by fun_prop) (.of_forall + fun ω N M hNM ↦ min_le_min_left _ (by exact_mod_cast hNM)) (.of_forall fun ω ↦ ?_) + simpa using (tendsto_const_nhds (x := X ω)).min ENNReal.tendsto_nat_nhds_top + obtain ⟨N, hNQ, hN2⟩ := ((h_tendsto.eventually (lt_mem_nhds hXQ)).and + (eventually_ge_atTop 2)).exists + exact ⟨fun ω ↦ min (X ω) N, N, hN2, hX.min_const (by exact_mod_cast (by omega : 1 ≤ N)), + fun ω ↦ min_le_right _ _, hNQ⟩ + +/-- A measure `Q` is outside the effective null of a null `S` of probability measures exactly +when, for some level `α ∈ (0, 1)`, some level-`α` test `φ` for `S` (a measurable function with +values in `[0, 1]` and expectation at most `α` under every member of `S`) has expectation larger +than `α` under `Q` [RW, Theorem 6.10]. -/ +theorem exists_powered_test_iff (hS : ∀ P ∈ S, IsProbabilityMeasure P) (Q : Measure Ω) : + (∃ α : ℝ≥0∞, 0 < α ∧ α < 1 ∧ ∃ φ : Ω → ℝ≥0∞, Measurable φ ∧ (∀ ω, φ ω ≤ 1) ∧ + (∀ P ∈ S, ∫⁻ ω, φ ω ∂P ≤ α) ∧ α < ∫⁻ ω, φ ω ∂Q) ↔ Q ∉ effectiveSet S := by + -- Both directions pass between a level-`α` test `φ` and the `[0, α⁻¹]`-valued e-variable + -- `α⁻¹ * φ` [RW, Fact 3.6]. + constructor + · rintro ⟨α, hα0, hα1, φ, hφ, -, hφS, hφQ⟩ hQ + -- `α⁻¹ * φ` is an e-variable for `S`, so its expectation under `Q` is at most `1`. + have hX : IsEVar (fun ω ↦ α⁻¹ * φ ω) S := by + refine .of_lintegral_le_one hS (measurable_const.mul hφ) fun P hP ↦ ?_ + rw [lintegral_const_mul _ hφ] + exact ENNReal.inv_mul_le_iff hα0.ne' (hα1.trans ENNReal.one_lt_top).ne |>.mpr <| + by simpa using hφS P hP + have h := hQ _ hX + rw [lintegral_const_mul _ hφ, + ENNReal.inv_mul_le_iff hα0.ne' (hα1.trans ENNReal.one_lt_top).ne, mul_one] at h + exact (h.trans_lt hφQ).false + · -- A bounded e-variable with expectation larger than `1` under `Q`, divided by its bound `N`, + -- is a level-`N⁻¹` test with power larger than `N⁻¹` under `Q`. + intro hQ + obtain ⟨Y, N, hN2, hY, hYN, hYQ⟩ := exists_isEVar_le_lt_lintegral_of_notMem_effectiveSet hQ + have hYm := hY.measurable + have hN0 : (N : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : N ≠ 0) + have hNtop : (N : ℝ≥0∞) ≠ ∞ := ENNReal.natCast_ne_top N + refine ⟨(N : ℝ≥0∞)⁻¹, ENNReal.inv_pos.mpr hNtop, ENNReal.inv_lt_one.mpr + (by exact_mod_cast (by omega : 1 < N)), fun ω ↦ (N : ℝ≥0∞)⁻¹ * Y ω, by fun_prop, + fun ω ↦ ?_, fun P hP ↦ ?_, ?_⟩ + · calc (N : ℝ≥0∞)⁻¹ * Y ω ≤ (N : ℝ≥0∞)⁻¹ * N := by gcongr; exact hYN ω + _ = 1 := ENNReal.inv_mul_cancel hN0 hNtop + · have := hS P hP + rw [lintegral_const_mul _ hYm] + calc (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, Y ω ∂P ≤ (N : ℝ≥0∞)⁻¹ * 1 := by + gcongr; simpa using hY.lintegral_le_measure_univ P hP + _ = (N : ℝ≥0∞)⁻¹ := mul_one _ + · rw [lintegral_const_mul _ hYm] + calc (N : ℝ≥0∞)⁻¹ = (N : ℝ≥0∞)⁻¹ * 1 := (mul_one _).symm + _ < (N : ℝ≥0∞)⁻¹ * ∫⁻ ω, Y ω ∂Q := + ENNReal.mul_lt_mul_right (ENNReal.inv_ne_zero.mpr hNtop) (ENNReal.inv_ne_top.mpr hN0) + hYQ + +end ProbabilityTheory diff --git a/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean b/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean index 24bcbe51..fec78f25 100644 --- a/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean +++ b/LMLExplore/MeasureTheory/Integral/Lebesgue/Add.lean @@ -6,20 +6,34 @@ Authors: LMLExplore contributors module public import Mathlib.MeasureTheory.Integral.Lebesgue.Add +public import Mathlib.Order.Filter.ENNReal +public import TauCeti.Topology.Instances.ENNReal /-! -# Lebesgue integral of a finite sum of indicators +# Lebesgue integral of finite sums and lower semicontinuity under setwise convergence ## Main statements * `MeasureTheory.lintegral_finsetSum_indicator_one`: the Lebesgue integral of a finite sum of indicators of measurable sets is the sum of their measures, and `MeasureTheory.lintegral_finsetSum_indicator_one₀`, its version for null measurable sets. +* `MeasureTheory.SimpleFunc.tendsto_lintegral_of_tendsto_measure`: the integral of a simple function + with finite values is continuous for the setwise convergence of measures. +* `MeasureTheory.SimpleFunc.lintegral_le_liminf_lintegral`: the integral of a simple function with + finite values is lower semicontinuous when the measures of measurable sets are. +* `MeasureTheory.lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure`: + if `μ s ≤ liminf (μs i s)` along a filter for every measurable set `s`, then + `∫⁻ f ∂μ ≤ liminf (∫⁻ f ∂μs i)` for every measurable `f`; in particular the Lebesgue integral + is lower semicontinuous for the setwise convergence of measures. This is the measurable-set + counterpart of the portmanteau inequality + `MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure`. -/ public section -open scoped ENNReal +open Filter + +open scoped ENNReal Topology namespace MeasureTheory @@ -39,4 +53,49 @@ lemma lintegral_finsetSum_indicator_one (hS : ∀ i ∈ s, MeasurableSet (S i)) ∫⁻ a, ∑ i ∈ s, (S i).indicator 1 a ∂μ = ∑ i ∈ s, μ (S i) := lintegral_finsetSum_indicator_one₀ fun i hi ↦ (hS i hi).nullMeasurableSet +section Setwise + +variable {ι : Type*} {l : Filter ι} {μs : ι → Measure α} + +/-- The integral of a simple function with finite values is continuous for the setwise convergence +of measures. -/ +theorem SimpleFunc.tendsto_lintegral_of_tendsto_measure (f : SimpleFunc α ℝ≥0∞) + (hf : ∀ y ∈ f.range, y ≠ ∞) + (h : ∀ s, MeasurableSet s → Tendsto (fun i ↦ μs i s) l (𝓝 (μ s))) : + Tendsto (fun i ↦ f.lintegral (μs i)) l (𝓝 (f.lintegral μ)) := by + unfold SimpleFunc.lintegral + exact tendsto_finsetSum _ fun y hy ↦ + ENNReal.Tendsto.const_mul (h _ (f.measurableSet_preimage _)) (.inr (hf y hy)) + +/-- The integral of a simple function with finite values is lower semicontinuous along a filter +when the measures of measurable sets are: if `μ s ≤ liminf (μs i s)` for every measurable set +`s`, then `f.lintegral μ ≤ liminf (f.lintegral (μs i))`. -/ +theorem SimpleFunc.lintegral_le_liminf_lintegral [l.NeBot] (f : SimpleFunc α ℝ≥0∞) + (hf : ∀ y ∈ f.range, y ≠ ∞) (h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l) : + f.lintegral μ ≤ liminf (fun i ↦ f.lintegral (μs i)) l := by + unfold SimpleFunc.lintegral + refine (Finset.sum_le_sum fun y hy ↦ ?_).trans (ENNReal.sum_liminf_le_liminf_sum _ _) + rw [ENNReal.liminf_const_mul_of_ne_top (hf y hy)] + gcongr + exact h _ (f.measurableSet_preimage _) + +/-- **Lower semicontinuity of the Lebesgue integral.** If `μ s ≤ liminf (μs i s)` along a filter +for every measurable set `s`, then `∫⁻ f ∂μ ≤ liminf (∫⁻ f ∂μs i)` for every measurable `f`. This +covers the setwise convergence of measures along any filter, so it holds for nets of measures and +not only for sequences. -/ +theorem lintegral_le_liminf_lintegral_of_forall_measurableSet_measure_le_liminf_measure [l.NeBot] + {f : α → ℝ≥0∞} (hf : Measurable f) + (h : ∀ s, MeasurableSet s → μ s ≤ liminf (fun i ↦ μs i s) l) : + ∫⁻ x, f x ∂μ ≤ liminf (fun i ↦ ∫⁻ x, f x ∂μs i) l := by + rw [lintegral_eq_iSup_eapprox_lintegral hf] + refine iSup_le fun n ↦ ?_ + refine ((SimpleFunc.eapprox f n).lintegral_le_liminf_lintegral (fun y hy ↦ ?_) h).trans + (liminf_le_liminf (.of_forall fun i ↦ ?_)) + · obtain ⟨x, rfl⟩ := SimpleFunc.mem_range.mp hy + exact (SimpleFunc.eapprox_lt_top f n x).ne + · rw [lintegral_eq_iSup_eapprox_lintegral hf] + exact le_iSup (fun n ↦ (SimpleFunc.eapprox f n).lintegral (μs i)) n + +end Setwise + end MeasureTheory