ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ<VAR>f g : α → ENNReal<VAR>hf : AEMeasurable f μ<VAR>hp0 : 0 ≤ p<VAR>hp1 : p ≤ 1<GOAL>(∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ 2 ^ (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → NNReal<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), ↑((f * g) a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>IsPiSystem {s | MeasurableSet s}
<VAR>α : Type u_1<VAR>S : Set α<GOAL>IsPiSystem {S}
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h_pi : IsPiSystem S<GOAL>IsPiSystem (insert ∅ S)
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h_pi : IsPiSystem S<GOAL>IsPiSystem (insert Set.univ S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set (Set β)<VAR>h_pi : IsPiSystem S<VAR>f : α → β<GOAL>IsPiSystem {s | ∃ t ∈ S, f ⁻¹' t = s}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>p : ι → Set (Set α)<VAR>hp_pi : ∀ (n : ι), IsPiSystem (p n)<VAR>hp_directed : Directed (fun x x_1 => x ≤ x_1) p<GOAL>IsPiSystem (⋃ n, p n)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>SemilatticeSup ι<VAR>p : ι → Set (Set α)<VAR>hp_pi : ∀ (n : ι), IsPiSystem (p n)<VAR>hp_mono : Monotone p<GOAL>IsPiSystem (⋃ n, p n)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>IsPiSystem (Set.Iio '' s)
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>IsPiSystem (Set.range Set.Iio)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>IsPiSystem (Set.Ioi '' s)
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>IsPiSystem (Set.range Set.Ioi)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>IsPiSystem (Set.Iic '' s)
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>IsPiSystem (Set.range Set.Iic)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>IsPiSystem (Set.Ici '' s)
<VAR>α : Type u_1<VAR>LinearOrder α<GOAL>IsPiSystem (Set.range Set.Ici)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>Ixx : α → α → Set α<VAR>p : α → α → Prop<VAR>Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b<VAR>Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)<VAR>s t : Set α<GOAL>IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, p l u ∧ Ixx l u = S}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>LinearOrder α<VAR>Ixx : α → α → Set α<VAR>p : α → α → Prop<VAR>Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b<VAR>Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)<VAR>f : ι → α<VAR>g : ι' → α<GOAL>IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ioo l u = S}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>LinearOrder α<VAR>f : ι → α<VAR>g : ι' → α<GOAL>IsPiSystem {S | ∃ l u, f l < g u ∧ Set.Ioo (f l) (g u) = S}
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ioc l u = S}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>LinearOrder α<VAR>f : ι → α<VAR>g : ι' → α<GOAL>IsPiSystem {S | ∃ i j, f i < g j ∧ Set.Ioc (f i) (g j) = S}
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Set.Ico l u = S}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>LinearOrder α<VAR>f : ι → α<VAR>g : ι' → α<GOAL>IsPiSystem {S | ∃ i j, f i < g j ∧ Set.Ico (f i) (g j) = S}
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>IsPiSystem {S | ∃ l ∈ s, ∃ u ∈ t, l ≤ u ∧ Set.Icc l u = S}
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>ι' : Sort u_3<VAR>LinearOrder α<VAR>f : ι → α<VAR>g : ι' → α<GOAL>IsPiSystem {S | ∃ i j, f i ≤ g j ∧ Set.Icc (f i) (g j) = S}
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>IsPiSystem (generatePiSystem S)
<VAR>α : Type u_1<VAR>S : Set (Set α)<GOAL>S ⊆ generatePiSystem S
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h_S : IsPiSystem S<GOAL>generatePiSystem S ⊆ S
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h_pi : IsPiSystem S<GOAL>generatePiSystem S = S
<VAR>α : Type u_1<VAR>S T : Set (Set α)<VAR>hST : S ⊆ T<GOAL>generatePiSystem S ⊆ generatePiSystem T
<VAR>α : Type u_1<VAR>M : MeasurableSpace α<VAR>S : Set (Set α)<VAR>h_meas_S : ∀ s ∈ S, MeasurableSet s<VAR>t : Set α<VAR>h_in_pi : t ∈ generatePiSystem S<GOAL>MeasurableSet t
<VAR>α : Type u_1<VAR>g : Set (Set α)<VAR>t : Set α<VAR>ht : t ∈ generatePiSystem g<GOAL>MeasurableSet t
<VAR>α : Type u_1<VAR>g : Set (Set α)<GOAL>MeasurableSpace.generateFrom (generatePiSystem g) = MeasurableSpace.generateFrom g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → Set (Set α)<VAR>h_pi : ∀ (b : β), IsPiSystem (g b)<VAR>t : Set α<VAR>h_t : t ∈ generatePiSystem (⋃ b, g b)<GOAL>∃ T f, t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>i : ι<GOAL>piiUnionInter π {i} = π i ∪ {Set.univ}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<GOAL>piiUnionInter (fun i => {s i}) S = {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s : ι → Set α<VAR>S : Set ι<GOAL>MeasurableSpace.generateFrom (piiUnionInter (fun k => {s k}) S) = MeasurableSpace.generateFrom {t | ∃ k ∈ S, s k = t}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>hpi : ∀ (x : ι), IsPiSystem (π x)<VAR>S : Set ι<GOAL>IsPiSystem (piiUnionInter π S)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π π' : ι → Set (Set α)<VAR>h_le : ∀ (i : ι), π i ⊆ π' i<VAR>S : Set ι<GOAL>piiUnionInter π S ⊆ piiUnionInter π' S
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>S T : Set ι<VAR>hST : S ⊆ T<GOAL>piiUnionInter π S ⊆ piiUnionInter π T
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace α<VAR>π : ι → Set (Set α)<VAR>h : ∀ (n : ι), MeasurableSpace.generateFrom (π n) ≤ m<VAR>S : Set ι<GOAL>MeasurableSpace.generateFrom (piiUnionInter π S) ≤ m
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<VAR>i : ι<VAR>hiS : i ∈ S<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>s ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>π : ι → Set (Set α)<VAR>S : Set ι<VAR>x : ι<VAR>hxS : x ∈ S<GOAL>MeasurableSpace.generateFrom (π x) ≤ MeasurableSpace.generateFrom (piiUnionInter π S)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<VAR>t : Set α<VAR>ht : t ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S<GOAL>MeasurableSet t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<GOAL>MeasurableSpace.generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i
<VAR>α : Type u_2<VAR>self : MeasurableSpace.DynkinSystem α<VAR>f : ℕ → Set α<GOAL>Pairwise (Disjoint on f) → (∀ (i : ℕ), self.Has (f i)) → self.Has (⋃ i, f i)
<VAR>α : Type u_2<VAR>self : MeasurableSpace.DynkinSystem α<GOAL>self.Has ∅
<VAR>α : Type u_2<VAR>self : MeasurableSpace.DynkinSystem α<VAR>a : Set α<GOAL>self.Has a → self.Has aᶜ
<VAR>α : Type u_1<VAR>d₁ d₂ : MeasurableSpace.DynkinSystem α<GOAL>(∀ (s : Set α), d₁.Has s ↔ d₂.Has s) → d₁ = d₂
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<VAR>a : Set α<GOAL>d.Has aᶜ ↔ d.Has a
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<GOAL>d.Has Set.univ
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<VAR>β : Type u_2<VAR>Countable β<VAR>f : β → Set α<VAR>hd : Pairwise (Disjoint on f)<VAR>h : ∀ (i : β), d.Has (f i)<GOAL>d.Has (⋃ i, f i)
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : Disjoint s₁ s₂<GOAL>d.Has (s₁ ∪ s₂)
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<VAR>s₁ s₂ : Set α<VAR>h₁ : d.Has s₁<VAR>h₂ : d.Has s₂<VAR>h : s₂ ⊆ s₁<GOAL>d.Has (s₁ \ s₂)
<VAR>α : Type u_2<VAR>a b : MeasurableSpace.DynkinSystem α<GOAL>a ≤ b ↔ a.Has ≤ b.Has
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasurableSpace α<GOAL>MeasurableSpace.DynkinSystem.ofMeasurableSpace m₁ ≤ MeasurableSpace.DynkinSystem.ofMeasurableSpace m₂ ↔ m₁ ≤ m₂
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<GOAL>MeasurableSpace.DynkinSystem.GenerateHas C sᶜ ↔ MeasurableSpace.DynkinSystem.GenerateHas C s
<VAR>α : Type u_1<VAR>C : Set (Set α)<GOAL>(MeasurableSpace.DynkinSystem.generate C).Has = MeasurableSpace.DynkinSystem.GenerateHas C
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<VAR>h_inter : ∀ (s₁ s₂ : Set α), d.Has s₁ → d.Has s₂ → d.Has (s₁ ∩ s₂)<GOAL>MeasurableSpace.DynkinSystem.ofMeasurableSpace (d.toMeasurableSpace h_inter) = d
<VAR>α : Type u_1<VAR>d : MeasurableSpace.DynkinSystem α<VAR>s : Set (Set α)<VAR>h : ∀ t ∈ s, d.Has t<GOAL>MeasurableSpace.DynkinSystem.generate s ≤ d
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>hs : (MeasurableSpace.DynkinSystem.generate C).Has s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>hs : IsPiSystem s<VAR>t₁ t₂ : Set α<VAR>ht₁ : (MeasurableSpace.DynkinSystem.generate s).Has t₁<VAR>ht₂ : (MeasurableSpace.DynkinSystem.generate s).Has t₂<GOAL>(MeasurableSpace.DynkinSystem.generate s).Has (t₁ ∩ t₂)
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>hs : IsPiSystem s<GOAL>MeasurableSpace.generateFrom s = (MeasurableSpace.DynkinSystem.generate s).toMeasurableSpace ⋯
<VAR>α : Type u_1<VAR>C : Set α → Prop<VAR>s : Set (Set α)<VAR>m : MeasurableSpace α<VAR>h_eq : m = MeasurableSpace.generateFrom s<VAR>h_inter : IsPiSystem s<VAR>h_empty : C ∅<VAR>h_basic : ∀ t ∈ s, C t<VAR>h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ<VAR>h_union : ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ i, f i)<VAR>t : Set α<GOAL>MeasurableSet t → C t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), ↑f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(↑f x) ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>ε : ℝ≥0∞<VAR>εpos : ε ≠ 0<GOAL>∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : Measurable f<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fint : MeasureTheory.Integrable (fun x => ↑(f x)) μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(↑f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), g x ≤ ↑f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(↑f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>f : α → ℝ≥0<VAR>fint : MeasureTheory.Integrable (fun x => ↑(f x)) μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ MeasureTheory.Integrable (fun x => ↑(g x)) μ ∧ ∫ (x : α), ↑(f x) ∂μ - ε ≤ ∫ (x : α), ↑(g x) ∂μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, g x < ⊤) ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ.WeaklyRegular<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∃ g, (∀ (x : α), g x < ↑(f x)) ∧ UpperSemicontinuous g ∧ MeasureTheory.Integrable (fun x => (g x).toReal) μ ∧ (∀ᵐ (x : α) ∂μ, ⊥ < g x) ∧ ∫ (x : α), f x ∂μ < ∫ (x : α), (g x).toReal ∂μ + ε
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>LinearOrder R<VAR>g : α → R<GOAL>{t | μ {a | t ≤ g a} ≠ μ {a | t < g a}}.Countable
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>R : Type u_3<VAR>LinearOrder R<VAR>MeasurableSpace R<VAR>ν : MeasureTheory.Measure R<VAR>MeasureTheory.NoAtoms ν<VAR>g : α → R<GOAL>(fun t => μ {a | t ≤ g a}) =ᵐ[ν] fun t => μ {a | t < g a}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ f<VAR>f_mble : Measurable f<VAR>g_intble : ∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t<VAR>g_mble : Measurable g<VAR>g_nn : ∀ t > 0, 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_mble : AEMeasurable f μ<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_mble : AEMeasurable f μ<VAR>g_intble : ∀ t > 0, IntervalIntegrable g MeasureTheory.volume 0 t<VAR>g_nn : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a} * ENNReal.ofReal (g t)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_mble : AEMeasurable f μ<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t < f a}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>f_intble : MeasureTheory.Integrable f μ<VAR>f_nn : 0 ≤ᵐ[μ] f<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, (μ {a | t < f a}).toReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>f_intble : MeasureTheory.Integrable f μ<VAR>f_nn : 0 ≤ᵐ[μ] f<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, (μ {a | t ≤ f a}).toReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>M : ℝ<VAR>f_intble : MeasureTheory.Integrable f μ<VAR>f_nn : 0 ≤ᵐ[μ] f<VAR>f_bdd : f ≤ᵐ[μ] fun x => M<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioc 0 M, (μ {a | t ≤ f a}).toReal
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SMul M α<VAR>MeasurableSMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>c : Mᵈᵐᵃ<VAR>f : α →ₘ[μ] β<GOAL>↑(c • f) =ᵐ[μ] fun x => ↑f (DomMulAct.mk.symm c • x)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>VAdd M α<VAR>MeasurableVAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>c : Mᵈᵃᵃ<VAR>f : α →ₘ[μ] β<GOAL>↑(c +ᵥ f) =ᵐ[μ] fun x => ↑f (DomAddAct.mk.symm c +ᵥ x)
<VAR>M : Type u_3<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SMul M α<VAR>MeasurableSMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>c : M<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>DomMulAct.mk c • MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (fun x => f (c • x)) ⋯
<VAR>M : Type u_3<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>VAdd M α<VAR>MeasurableVAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>c : M<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>DomAddAct.mk c +ᵥ MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (fun x => f (c +ᵥ x)) ⋯
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>VAdd M α<VAR>MeasurableVAdd M α<VAR>MeasureTheory.VAddInvariantMeasure M α μ<VAR>c : Mᵈᵃᵃ<VAR>b : β<GOAL>c +ᵥ MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.const α b
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>MeasurableSpace M<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>SMul M α<VAR>MeasurableSMul M α<VAR>MeasureTheory.SMulInvariantMeasure M α μ<VAR>c : Mᵈᵐᵃ<VAR>b : β<GOAL>c • MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.const α b
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>f : α → β → E<VAR>hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)<GOAL>MeasurableSet {x | MeasureTheory.Integrable (f x) ν}
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite ν<VAR>f : α → β → E<VAR>hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)<GOAL>MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → E<VAR>hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)<GOAL>MeasureTheory.StronglyMeasurable fun y => ∫ (x : α), f x y ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.StronglyMeasurable fun y => ∫ (x : α), f (x, y) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>h2s : (μ.prod ν) s ≠ ⊤<GOAL>MeasureTheory.Integrable (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>γ : Type u_7<VAR>TopologicalSpace γ<VAR>MeasureTheory.SFinite μ<VAR>MeasureTheory.SFinite ν<VAR>f : β × α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f (ν.prod μ)<GOAL>MeasureTheory.AEStronglyMeasurable (fun z => f z.swap) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>γ : Type u_7<VAR>TopologicalSpace γ<VAR>MeasureTheory.SFinite ν<VAR>f : α → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.AEStronglyMeasurable (fun z => f z.1) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>γ : Type u_7<VAR>TopologicalSpace γ<VAR>MeasureTheory.SFinite ν<VAR>f : β → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f ν<GOAL>MeasureTheory.AEStronglyMeasurable (fun z => f z.2) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>f : α × β → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : β), f (x, y) ∂ν) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>γ : Type u_7<VAR>MeasureTheory.SFinite ν<VAR>TopologicalSpace γ<VAR>f : α × β → γ<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)<GOAL>∀ᵐ (x : α) ∂μ, MeasureTheory.AEStronglyMeasurable (fun y => f (x, y)) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<GOAL>MeasureTheory.Integrable (f ∘ Prod.swap) (ν.prod μ) ↔ MeasureTheory.Integrable f (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>MeasureTheory.Integrable (f ∘ Prod.swap) (ν.prod μ)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → E<VAR>h1f : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.HasFiniteIntegral f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) ν) ∧ MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → E<VAR>h1f : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)<GOAL>MeasureTheory.HasFiniteIntegral f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) ν) ∧ MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ