ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>hb : μ {b} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>ha : μ {a} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Ico a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>hb : μ {b} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>ha : μ {a} ≠ ⊤<VAR>hb : μ {b} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>b : α<VAR>hb : μ {b} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>b : α<VAR>hb : μ {b} ≠ ⊤<GOAL>MeasureTheory.IntegrableOn f (Set.Iic b) μ ↔ MeasureTheory.IntegrableOn f (Set.Iio b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Ico a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>a b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Ici b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioi b) μ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>PartialOrder α<VAR>MeasurableSingletonClass α<VAR>f : α → E<VAR>μ : MeasureTheory.Measure α<VAR>b : α<VAR>MeasureTheory.NoAtoms μ<GOAL>MeasureTheory.IntegrableOn f (Set.Iic b) μ ↔ MeasureTheory.IntegrableOn f (Set.Iio b) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<GOAL>Function.Periodic (Complex.circleTransformDeriv R z w f) (2 * π)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<GOAL>Complex.circleTransformDeriv R z w f = fun θ => (circleMap z R θ - w)⁻¹ • Complex.circleTransform R z w f θ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<GOAL>∫ (θ : ℝ) in 0 ..2 * π, Complex.circleTransform R z w f θ = (2 * ↑π * Complex.I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (Metric.sphere z R)<VAR>hw : w ∈ Metric.ball z R<GOAL>Continuous (Complex.circleTransform R z w f)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (Metric.sphere z R)<VAR>hw : w ∈ Metric.ball z R<GOAL>Continuous (Complex.circleTransformDeriv R z w f)
<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<GOAL>ContinuousOn (fun w => (circleMap z R w.2 - w.1)⁻¹ ^ 2) (Metric.closedBall z r ×ˢ Set.univ)
<VAR>R r : ℝ<VAR>hr : r < R<VAR>z : ℂ<GOAL>ContinuousOn (⇑Complex.abs ∘ Complex.circleTransformBoundingFunction R z) (Metric.closedBall z r ×ˢ Set.univ)
<VAR>R r : ℝ<VAR>hr : r < R<VAR>hr' : 0 ≤ r<VAR>z : ℂ<GOAL>∃ x, ∀ (y : ↑(Metric.closedBall z r ×ˢ [[0, 2 * π]])), Complex.abs (Complex.circleTransformBoundingFunction R z ↑y) ≤ Complex.abs (Complex.circleTransformBoundingFunction R z ↑x)
<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ Metric.ball z R<VAR>hf : ContinuousOn f (Metric.sphere z R)<GOAL>∃ B ε, 0 < ε ∧ Metric.ball x ε ⊆ Metric.ball z R ∧ ∀ (t : ℝ), ∀ y ∈ Metric.ball x ε, ‖Complex.circleTransformDeriv R z y f t‖ ≤ B
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.IsSetSemiring C<VAR>s : Set α<GOAL>s ∈ C → ∀ t ∈ C, s ∩ t ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.IsSetSemiring C<GOAL>∅ ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.IsSetSemiring C<VAR>s : Set α<GOAL>s ∈ C → ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<GOAL>IsPiSystem C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>∅ ∉ hC.diffFinset hs ht
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>↑(hC.diffFinset hs ht) ⊆ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>(↑(hC.diffFinset hs ht)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>⋃₀ ↑(hC.diffFinset hs ht) = s \ t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>t ∉ hC.diffFinset hs ht
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : t ⊆ s<GOAL>⋃₀ insert t ↑(hC.diffFinset hs ht) = s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>Disjoint t (⋃₀ ↑(hC.diffFinset hs ht))
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>(insert t ↑(hC.diffFinset hs ht)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I = ⋃₀ ↑J
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>∅ ∉ hC.diffFinset₀ hs hI
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>↑(hC.diffFinset₀ hs hI) ⊆ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>(↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>s \ ⋃₀ ↑I = ⋃₀ ↑(hC.diffFinset₀ hs hI)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>⋃₀ ↑(hC.diffFinset₀ hs hI) ⊆ s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.diffFinset₀ hs hI))
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>Disjoint I (hC.diffFinset₀ hs hI)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<GOAL>(↑I ∪ ↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<GOAL>⋃₀ ↑I ∪ ⋃₀ ↑(hC.diffFinset₀ hs hI) = s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<VAR>DecidableEq (Set α)<GOAL>⋃₀ ↑(I ∪ hC.diffFinset₀ hs hI) = s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.IsSetRing C<VAR>s t : Set α<GOAL>s ∈ C → t ∈ C → s ∪ t ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.IsSetRing C<VAR>s t : Set α<GOAL>s ∈ C → t ∈ C → s \ t ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.IsSetRing C<GOAL>∅ ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : MeasureTheory.IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>s ∩ t ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>hC : MeasureTheory.IsSetRing C<GOAL>MeasureTheory.IsSetSemiring C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>ι : Type u_2<VAR>hC : MeasureTheory.IsSetRing C<VAR>s : ι → Set α<VAR>S : Finset ι<VAR>hs : ∀ n ∈ S, s n ∈ C<GOAL>⋃ i ∈ S, s i ∈ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>ι : Type u_2<VAR>hC : MeasureTheory.IsSetRing C<VAR>s : ι → Set α<VAR>S : Finset ι<VAR>hS : S.Nonempty<VAR>hs : ∀ n ∈ S, s n ∈ C<GOAL>⋂ i ∈ S, s i ∈ C
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : X →ᵇ ℝ≥0<VAR>x : X<GOAL>f x ≤ nndist 0 f
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>f : X →ᵇ ℝ≥0<VAR>μ : MeasureTheory.Measure X<GOAL>∫⁻ (x : X), ↑(f x) ∂μ ≤ edist 0 f * μ Set.univ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>f : X →ᵇ ℝ≥0<GOAL>Measurable fun x => ↑(f x)
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>∫⁻ (x : X), ↑(f x) ∂μ < ⊤
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>MeasureTheory.Integrable (NNReal.toReal ∘ ⇑f) μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<GOAL>∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<GOAL>∫⁻ (x : X), ENNReal.ofReal (f x) ∂μ < ⊤
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>f : X →ᵇ ℝ≥0<VAR>μ : MeasureTheory.Measure X<GOAL>(∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>μ : MeasureTheory.Measure X<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>f : X →ᵇ E<GOAL>∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ↑‖f‖₊ * μ Set.univ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>MeasureTheory.Integrable (⇑f) μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>‖∫ (x : X), f x ∂μ‖ ≤ (μ Set.univ).toReal * ‖f‖
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>f : X →ᵇ E<GOAL>‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>TopologicalSpace X<VAR>OpensMeasurableSpace X<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>SecondCountableTopology E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>NormedSpace ℝ E<VAR>ι : Type u_3<VAR>μs : ι → MeasureTheory.Measure X<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>f : X →ᵇ E<GOAL>Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<VAR>c : ℝ<GOAL>∫ (x : X), (f + BoundedContinuousFunction.const X c) x ∂μ = ∫ (x : X), f x ∂μ + (μ Set.univ).toReal • c
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<VAR>c : ℝ<GOAL>∫ (x : X), (BoundedContinuousFunction.const X c - f) x ∂μ = (μ Set.univ).toReal • c - ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>μs : ι → MeasureTheory.Measure X<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → Filter.limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<GOAL>Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>μs : ι → MeasureTheory.Measure X<VAR>∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ Filter.liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<GOAL>Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>𝕜 : Type u_2<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>L : E →L[𝕜] F<GOAL>Measurable ⇑L
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>𝕜 : Type u_2<VAR>NormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>L : E →L[𝕜] F<VAR>φ : α → E<VAR>φ_meas : Measurable φ<GOAL>Measurable fun a => L (φ a)
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>x : E<GOAL>Measurable fun f => f x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>MeasurableSpace F<VAR>BorelSpace F<GOAL>Measurable fun x f => f x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>MeasurableSpace F<VAR>BorelSpace F<GOAL>Measurable fun f x => f x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>φ : α → F →L[𝕜] E<VAR>hφ : Measurable φ<VAR>v : F<GOAL>Measurable fun a => (φ a) v
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>φ : α → F →L[𝕜] E<VAR>μ : MeasureTheory.Measure α<VAR>hφ : AEMeasurable φ μ<VAR>v : F<GOAL>AEMeasurable (fun a => (φ a) v) μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>MeasurableSpace 𝕜<VAR>BorelSpace 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<GOAL>(Measurable fun x => f x • c) ↔ Measurable f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>MeasurableSpace 𝕜<VAR>BorelSpace 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → 𝕜<VAR>μ : MeasureTheory.Measure α<VAR>c : E<VAR>hc : c ≠ 0<GOAL>AEMeasurable (fun x => f x • c) μ ↔ AEMeasurable f μ
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x : ι → ℝ<VAR>h : ∀ (δ : ℝ), 0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior s<GOAL>¬Filter.Tendsto (fun r => MeasureTheory.volume (closure s ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 0)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x : ι → ℝ<VAR>h : ∀ (δ : ℝ), 0 < δ → ∃ y, Metric.closedBall y (δ / 4) ⊆ Metric.closedBall x δ ∧ Metric.closedBall y (δ / 4) ⊆ interior sᶜ<GOAL>¬Filter.Tendsto (fun r => MeasureTheory.volume (closure s ∩ Metric.closedBall x r) / MeasureTheory.volume (Metric.closedBall x r)) (𝓝[>] 0) (𝓝 1)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>hs : IsUpperSet s<GOAL>MeasureTheory.volume (frontier s) = 0
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>hs : IsLowerSet s<GOAL>MeasureTheory.volume (frontier s) = 0
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>hs : s.OrdConnected<GOAL>MeasureTheory.volume (frontier s) = 0
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>hs : s.OrdConnected<GOAL>MeasureTheory.NullMeasurableSet s MeasureTheory.volume
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<VAR>Nonempty ι<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>MeasureTheory.volume s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>ι : Type u_3<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>lim : Filter.Tendsto f u (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ℕ), Measurable (f i)<VAR>lim : Filter.Tendsto f Filter.atTop (𝓝 g)<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>ι : Type u_3<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → α → β<VAR>g : α → β<VAR>u : Filter ι<VAR>hu : u.NeBot<VAR>u.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (𝓝 (g x))<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_3<VAR>MeasurableSpace β<VAR>PseudoMetricSpace β<VAR>BorelSpace β<VAR>μ : MeasureTheory.Measure α<VAR>g : α → β<VAR>hf : ∀ ε > 0, ∃ f, AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε<GOAL>AEMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>μ : MeasureTheory.Measure α<VAR>μ.IsComplete<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (g x))<GOAL>Measurable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>ι : Type u_3<VAR>Countable ι<VAR>Nonempty ι<VAR>μ : MeasureTheory.Measure α<VAR>f : ι → α → β<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>hf : ∀ (n : ι), AEMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) L (𝓝 l)<GOAL>∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) L (𝓝 (f_lim x))
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_4<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>L.NeBot<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>MeasurableSet A
<VAR>α : Type u_3<VAR>MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_4<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>L.NeBot<VAR>μ : MeasureTheory.Measure α<VAR>As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>MeasureTheory.NullMeasurableSet A μ
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>MeasurableSet (Metric.ball x ε)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>MeasurableSet (Metric.closedBall x ε)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s : Set α<GOAL>Measurable fun x => Metric.infDist x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<GOAL>Measurable fun x => Metric.infDist (f x) s
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>s : Set α<GOAL>Measurable fun x => Metric.infNndist x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>s : Set α<GOAL>Measurable fun x => Metric.infNndist (f x) s
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>SecondCountableTopology α<GOAL>Measurable fun p => dist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>MeasurableSpace α<VAR>OpensMeasurableSpace α<VAR>MeasurableSpace β<VAR>SecondCountableTopology α<VAR>f g : β → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun b => dist (f b) (g b)