ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>Zero β<VAR>Zero γ<VAR>g : β → γ<VAR>hg : g 0 = 0<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<GOAL>MeasureTheory.SimpleFunc.map g (f.restrict s) = (MeasureTheory.SimpleFunc.map g f).restrict s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0<VAR>s : Set α<GOAL>MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (f.restrict s) = (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal f).restrict s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0<VAR>s : Set α<GOAL>MeasureTheory.SimpleFunc.map NNReal.toReal (f.restrict s) = (MeasureTheory.SimpleFunc.map NNReal.toReal f).restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>↑(f.restrict s) a = s.indicator (↑f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : 0 ∉ t<GOAL>↑(f.restrict s) ⁻¹' t = s ∩ ↑f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : β<VAR>hr : r ≠ 0<GOAL>↑(f.restrict s) ⁻¹' {r} = s ∩ ↑f ⁻¹' {r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>r : β<VAR>s : Set α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>hs : MeasurableSet s<GOAL>r ∈ (f.restrict s).range ↔ r = 0 ∧ s ≠ Set.univ ∨ r ∈ ↑f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>r : β<VAR>s : Set α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>hr : r ∈ (f.restrict s).range<VAR>h0 : r ≠ 0<GOAL>r ∈ ↑f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>Preorder β<VAR>s : Set α<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>H : f ≤ g<GOAL>f.restrict s ≤ g.restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>Zero β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<GOAL>↑(MeasureTheory.SimpleFunc.approx i f n) a = (Finset.range n).sup fun k => if i k ≤ f a then i k else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>Zero β<VAR>i : ℕ → β<VAR>f : α → β<GOAL>Monotone (MeasureTheory.SimpleFunc.approx i f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>Zero β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>MeasurableSpace γ<VAR>i : ℕ → β<VAR>f : γ → β<VAR>g : α → γ<VAR>n : ℕ<VAR>a : α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>↑(MeasureTheory.SimpleFunc.approx i (f ∘ g) n) a = ↑(MeasureTheory.SimpleFunc.approx i f n) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>CompleteLattice β<VAR>OrderClosedTopology β<VAR>Zero β<VAR>MeasurableSpace β<VAR>OpensMeasurableSpace β<VAR>i : ℕ → β<VAR>f : α → β<VAR>a : α<VAR>hf : Measurable f<VAR>h_zero : 0 = ⊥<GOAL>⨆ n, ↑(MeasureTheory.SimpleFunc.approx i f n) a = ⨆ k, ⨆ (_ : i k ≤ f a), i k
<VAR>q : ℚ<GOAL>MeasureTheory.SimpleFunc.ennrealRatEmbed (Encodable.encode q) = ↑(↑q).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>n : ℕ<VAR>a : α<GOAL>↑(MeasureTheory.SimpleFunc.eapprox f n) a < ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<GOAL>Monotone (MeasureTheory.SimpleFunc.eapprox f)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>⨆ n, ↑(MeasureTheory.SimpleFunc.eapprox f n) a = f a
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace γ<VAR>f : γ → ℝ≥0∞<VAR>g : α → γ<VAR>n : ℕ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>↑(MeasureTheory.SimpleFunc.eapprox (f ∘ g) n) = ↑(MeasureTheory.SimpleFunc.eapprox f n) ∘ g
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>n : ℕ<VAR>a : α<GOAL>∑ k ∈ Finset.range (n + 1), ↑(↑(MeasureTheory.SimpleFunc.eapproxDiff f k) a) = ↑(MeasureTheory.SimpleFunc.eapprox f n) a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>∑' (n : ℕ), ↑(↑(MeasureTheory.SimpleFunc.eapproxDiff f n) a) = f a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : ∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s<GOAL>f.lintegral μ = ∑ x ∈ s, x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>s : Finset ℝ≥0∞<VAR>hs : f.range \ {0} ⊆ s<GOAL>f.lintegral μ = ∑ x ∈ s, x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>g : β → ℝ≥0∞<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>(MeasureTheory.SimpleFunc.map g f).lintegral μ = ∑ x ∈ f.range, g x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : MeasureTheory.SimpleFunc α ℝ≥0∞<GOAL>(f + g).lintegral μ = f.lintegral μ + g.lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>x : ℝ≥0∞<GOAL>(MeasureTheory.SimpleFunc.const α x * f).lintegral μ = x * f.lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.SimpleFunc.lintegral 0 μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<GOAL>f.lintegral (μ + ν) = f.lintegral μ + f.lintegral ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>c : ℝ≥0∞<GOAL>f.lintegral (c • μ) = c • f.lintegral μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<GOAL>f.lintegral 0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>μ : ι → MeasureTheory.Measure α<GOAL>f.lintegral (MeasureTheory.Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(f.restrict s).lintegral μ = ∑ r ∈ f.range, r * μ (↑f ⁻¹' {r} ∩ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<GOAL>f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (↑f ⁻¹' {y} ∩ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(f.restrict s).lintegral μ = f.lintegral (μ.restrict s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>Countable ι<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<VAR>μ : MeasureTheory.Measure α<GOAL>f.lintegral (μ.restrict (⋃ i, s i)) = ⨆ i, f.lintegral (μ.restrict (s i))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<GOAL>(MeasureTheory.SimpleFunc.const α c).lintegral μ = c * μ Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<GOAL>(MeasureTheory.SimpleFunc.const α c).lintegral (μ.restrict s) = c * μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((MeasureTheory.SimpleFunc.const α c).restrict s).lintegral μ = c * μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : MeasureTheory.SimpleFunc α ℝ≥0∞<GOAL>f.lintegral μ ⊔ g.lintegral μ ≤ (f ⊔ g).lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f g : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>hfg : f ≤ g<VAR>hμν : μ ≤ ν<GOAL>f.lintegral μ ≤ g.lintegral ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>g : MeasureTheory.SimpleFunc β ℝ≥0∞<VAR>ν : MeasureTheory.Measure β<VAR>H : ∀ (y : ℝ≥0∞), μ (↑f ⁻¹' {y}) = ν (↑g ⁻¹' {y})<GOAL>f.lintegral μ = g.lintegral ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>h : ↑f =ᵐ[μ] ↑g<GOAL>f.lintegral μ = g.lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>μ' : MeasureTheory.Measure β<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>g : MeasureTheory.SimpleFunc β ℝ≥0∞<VAR>m' : α → β<VAR>eq : ∀ (a : α), ↑f a = ↑g (m' a)<VAR>h : ∀ (s : Set β), MeasurableSet s → μ' s = μ (m' ⁻¹' s)<GOAL>f.lintegral μ = g.lintegral μ'
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>g : MeasureTheory.SimpleFunc β ℝ≥0∞<VAR>f : α → β<VAR>hf : Measurable f<GOAL>g.lintegral (MeasureTheory.Measure.map f μ) = (g.comp f hf).lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>Function.support ↑f = ⋃ y ∈ Finset.filter (fun y => y ≠ 0) f.range, ↑f ⁻¹' {y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<VAR>MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>MeasurableSet (Function.support ↑f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>f.FinMeasSupp μ ↔ μ (Function.support ↑f) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<GOAL>f.FinMeasSupp μ ↔ ∀ (y : β), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>h : f.FinMeasSupp μ<VAR>y : β<VAR>hy : y ≠ 0<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>Zero γ<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → γ<VAR>hf : f.FinMeasSupp μ<VAR>hg : g 0 = 0<GOAL>(MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>Zero γ<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → γ<VAR>h : (MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ<VAR>hg : ∀ (b : β), g b = 0 → b = 0<GOAL>f.FinMeasSupp μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>Zero γ<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : β → γ<VAR>hg : ∀ {b : β}, g b = 0 ↔ b = 0<GOAL>(MeasureTheory.SimpleFunc.map g f).FinMeasSupp μ ↔ f.FinMeasSupp μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>Zero γ<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>g : MeasureTheory.SimpleFunc α γ<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(f.pair g).FinMeasSupp μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>Zero β<VAR>Zero γ<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α β<VAR>Zero δ<VAR>hf : f.FinMeasSupp μ<VAR>g : MeasureTheory.SimpleFunc α γ<VAR>hg : g.FinMeasSupp μ<VAR>op : β → γ → δ<VAR>H : op 0 0 = 0<GOAL>(MeasureTheory.SimpleFunc.map (Function.uncurry op) (f.pair g)).FinMeasSupp μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>AddMonoid β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(f + g).FinMeasSupp μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>MonoidWithZero β<VAR>f g : MeasureTheory.SimpleFunc α β<VAR>hf : f.FinMeasSupp μ<VAR>hg : g.FinMeasSupp μ<GOAL>(f * g).FinMeasSupp μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>hm : f.FinMeasSupp μ<VAR>hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤<GOAL>f.lintegral μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>h : f.lintegral μ ≠ ⊤<GOAL>f.FinMeasSupp μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤<GOAL>f.FinMeasSupp μ ↔ f.lintegral μ < ⊤
<VAR>α : Type u_5<VAR>γ : Type u_6<VAR>MeasurableSpace α<VAR>AddMonoid γ<VAR>P : MeasureTheory.SimpleFunc α γ → Prop<VAR>h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))<VAR>h_add : ∀ ⦃f g : MeasureTheory.SimpleFunc α γ⦄, Disjoint (Function.support ↑f) (Function.support ↑g) → P f → P g → P (f + g)<VAR>f : MeasureTheory.SimpleFunc α γ<GOAL>P f
<VAR>α : Type u_1<VAR>E : Type u_5<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddGroup E] [inst_2 : MeasurableAdd E] {g : α → E}, Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (g + ↑f)
<VAR>α : Type u_1<VAR>E : Type u_5<GOAL>∀ {x : MeasurableSpace α} [inst : MeasurableSpace E] [inst_1 : AddGroup E] [inst_2 : MeasurableAdd E] {g : α → E}, Measurable g → ∀ (f : MeasureTheory.SimpleFunc α E), Measurable (↑f + g)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>P : (α → ℝ≥0∞) → Prop<VAR>h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (Function.support f) (Function.support g) → Measurable f → Measurable g → P f → P g → P (f + g)<VAR>h_iSup : ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ n, f n x<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>P f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<GOAL>MeasurableSet s ↔ MeasurableSet s ∧ f ⁻¹' s = s
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasurableSpace.invariants id = inst✝
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → α<GOAL>MeasurableSpace.invariants f ≤ inst✝
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f g : α → α<GOAL>MeasurableSpace.invariants f ⊓ MeasurableSpace.invariants g ≤ MeasurableSpace.invariants (f ∘ g)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → α<VAR>n : ℕ<GOAL>MeasurableSpace.invariants f ≤ MeasurableSpace.invariants f^[n]
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f : α → α<VAR>g : α → β<GOAL>Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ f ⁻¹' s = g ⁻¹' s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>fa : α → α<VAR>fb : β → β<VAR>g : α → β<VAR>hg : Measurable g<VAR>hfg : Function.Semiconj g fa fb<GOAL>Measurable g
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>m.IsCaratheodory s ↔ ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m.IsCaratheodory ∅
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ : Set α<GOAL>m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>m.IsCaratheodory sᶜ ↔ m.IsCaratheodory s
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<VAR>h₁ : m.IsCaratheodory s₁<VAR>h₂ : m.IsCaratheodory s₂<GOAL>m.IsCaratheodory (s₁ ∪ s₂)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<VAR>h : s₁ ∩ s₂ ⊆ ∅<VAR>h₁ : m.IsCaratheodory s₁<VAR>t : Set α<GOAL>m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<VAR>n : ℕ<GOAL>(∀ i < n, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i, ⋃ (_ : i < n), s i)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<VAR>h₁ : m.IsCaratheodory s₁<VAR>h₂ : m.IsCaratheodory s₂<GOAL>m.IsCaratheodory (s₁ ∩ s₂)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>t : Set α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>m.IsCaratheodory (⋃ i, s i)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), m.IsCaratheodory (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ (t : Set α), m t = m (t ∩ s) + m (t \ s)
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set α<GOAL>MeasurableSet s ↔ ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t
<VAR>α : Type u<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<VAR>h : ∀ (i : ℕ), MeasurableSet (s i)<VAR>hd : Pairwise (Disjoint on s)<GOAL>m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
<VAR>α : Type u_1<GOAL>MeasureTheory.OuterMeasure.caratheodory 0 = ⊤
<VAR>α : Type u_1<GOAL>⊤.caratheodory = ⊤
<VAR>α : Type u_1<VAR>m₁ m₂ : MeasureTheory.OuterMeasure α<GOAL>m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂).caratheodory
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasureTheory.OuterMeasure α<GOAL>⨅ i, (m i).caratheodory ≤ (MeasureTheory.OuterMeasure.sum m).caratheodory
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m.caratheodory ≤ (a • m).caratheodory
<VAR>α : Type u_1<VAR>a : α<GOAL>(MeasureTheory.OuterMeasure.dirac a).caratheodory = ⊤
<VAR>α : Type u_5<VAR>F' : Type u_6<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m : MeasurableSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<GOAL>μ[f|m] = if hm : m ≤ m0 then if h : MeasureTheory.SigmaFinite (μ.trim hm) ∧ MeasureTheory.Integrable f μ then if MeasureTheory.StronglyMeasurable f then f else MeasureTheory.AEStronglyMeasurable'.mk ↑↑(MeasureTheory.condexpL1 hm μ f) ⋯ else 0 else 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>hm_not : ¬m ≤ m0<GOAL>μ[f|m] = 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm_not : ¬MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>μ[f|m] = 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm : MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>μ[f|m] = if MeasureTheory.Integrable f μ then if MeasureTheory.StronglyMeasurable f then f else MeasureTheory.AEStronglyMeasurable'.mk ↑↑(MeasureTheory.condexpL1 hm μ f) ⋯ else 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hμm : MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>μ[f|m] = f
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>c : F'<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>μ[fun x => c|m] = fun x => c
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hμm : MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<GOAL>μ[f|m] =ᵐ[μ] ↑↑(MeasureTheory.condexpL1 hm μ f)
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hf : MeasureTheory.Integrable f μ<GOAL>μ[f|m] =ᵐ[μ] ↑↑((MeasureTheory.condexpL1CLM F' hm μ) (MeasureTheory.Integrable.toL1 f hf))
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>hf : ¬MeasureTheory.Integrable f μ<GOAL>μ[f|m] = 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ[0|m] = 0
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<GOAL>MeasureTheory.StronglyMeasurable (μ[f|m])
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → F'<VAR>h : f =ᵐ[μ] g<GOAL>μ[f|m] =ᵐ[μ] μ[g|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>hμm : MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : MeasureTheory.AEStronglyMeasurable' m f μ<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>μ[f|m] =ᵐ[μ] f
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<GOAL>MeasureTheory.Integrable (μ[f|m]) μ
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>hf : MeasureTheory.Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (μ[f|m]) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<VAR>hm : m ≤ m0<VAR>hμm : MeasureTheory.SigmaFinite (μ.trim hm)<GOAL>∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mF : MeasurableSpace F<VAR>Y : α → F<VAR>hY : Measurable Y<VAR>MeasureTheory.SigmaFinite (μ.trim ⋯)<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>∫ (x : α), (μ[A.indicator fun x => 1|MeasurableSpace.comap Y mF]) x ∂μ = (μ A).toReal
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ<VAR>hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ<VAR>hgm : MeasureTheory.AEStronglyMeasurable' m g μ<GOAL>g =ᵐ[μ] μ[f|m]
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hμ : NeZero μ<VAR>f : α → F'<GOAL>μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → F'<GOAL>μ[f|⊥] =ᵐ[μ] fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F' : Type u_3<VAR>NormedAddCommGroup F'<VAR>NormedSpace ℝ F'<VAR>CompleteSpace F'<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : α → F'<GOAL>μ[f|⊥] = fun x => ∫ (x : α), f x ∂μ