ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.FiniteMeasure α<VAR>ν : MeasureTheory.FiniteMeasure β<GOAL>(μ.prod ν).map Prod.swap = ν.prod μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<GOAL>↑(μ.prod ν) = (↑μ).prod ↑ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<VAR>s : Set (α × β)<VAR>s_mble : MeasurableSet s<GOAL>(μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) = μ s * ν t
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<GOAL>(μ.prod ν).map ⋯ = μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<GOAL>(μ.prod ν).map ⋯ = ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<VAR>α' : Type u_3<VAR>MeasurableSpace α'<VAR>β' : Type u_4<VAR>MeasurableSpace β'<VAR>f : α → α'<VAR>g : β → β'<VAR>f_mble : Measurable f<VAR>g_mble : Measurable g<GOAL>(μ.map ⋯).prod (ν.map ⋯) = (μ.prod ν).map ⋯
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.ProbabilityMeasure α<VAR>ν : MeasureTheory.ProbabilityMeasure β<GOAL>(μ.prod ν).map ⋯ = ν.prod μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ - ν = sInf {d | μ ≤ d + ν}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν d : MeasureTheory.Measure α<VAR>h : μ ≤ d + ν<GOAL>μ - ν ≤ d
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ≤ ν<GOAL>μ - ν = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ - ν ≤ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ - ⊤ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>0 - μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ - μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>h₁ : MeasurableSet s<VAR>h₂ : ν ≤ μ<GOAL>(μ - ν) s = μ s - ν s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure ν<VAR>h₁ : ν ≤ μ<GOAL>μ - ν + ν = μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>h_meas_s : MeasurableSet s<GOAL>(μ - ν).restrict s = μ.restrict s - ν.restrict s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>h_le : μ.restrict s ≤ ν.restrict s<VAR>h_meas_s : MeasurableSet s<GOAL>(μ - ν) s = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : μ s = 0<VAR>ht : ν t = 0<VAR>hst : Set.univ ⊆ s ∪ t<GOAL>μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<GOAL>MeasurableSet h.nullSet
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<GOAL>μ h.nullSet = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<GOAL>ν h.nullSetᶜ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<GOAL>μ.restrict h.nullSet = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<GOAL>ν.restrict h.nullSetᶜ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ ⟂ₘ 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : ν ⟂ₘ μ<GOAL>μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<GOAL>μ ⟂ₘ ν ↔ ν ⟂ₘ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>0 ⟂ₘ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α<VAR>h : μ₁ ⟂ₘ ν₁<VAR>hμ : μ₂ ≪ μ₁<VAR>hν : ν₂ ≪ ν₁<GOAL>μ₂ ⟂ₘ ν₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α<VAR>h : μ₁ ⟂ₘ ν₁<VAR>hμ : μ₂ ≤ μ₁<VAR>hν : ν₂ ≤ ν₁<GOAL>μ₂ ⟂ₘ ν₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ ⟂ₘ μ ↔ μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>ν : MeasureTheory.Measure α<VAR>ι : Type u_2<VAR>Countable ι<VAR>μ : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.Measure.sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_2<VAR>Countable ι<VAR>ν : ι → MeasureTheory.Measure α<GOAL>μ ⟂ₘ MeasureTheory.Measure.sum ν ↔ ∀ (i : ι), μ ⟂ₘ ν i
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ₁ μ₂ ν : MeasureTheory.Measure α<GOAL>μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν₁ ν₂ : MeasureTheory.Measure α<GOAL>μ ⟂ₘ ν₁ + ν₂ ↔ μ ⟂ₘ ν₁ ∧ μ ⟂ₘ ν₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν₁ ν₂ : MeasureTheory.Measure α<VAR>h₁ : ν₁ ⟂ₘ μ<VAR>h₂ : ν₂ ⟂ₘ μ<GOAL>ν₁ + ν₂ ⟂ₘ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν₁ ν₂ : MeasureTheory.Measure α<VAR>h₁ : μ ⟂ₘ ν₁<VAR>h₂ : μ ⟂ₘ ν₂<GOAL>μ ⟂ₘ ν₁ + ν₂
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>h : ν ⟂ₘ μ<GOAL>r • ν ⟂ₘ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>r : ℝ≥0<VAR>h : ν ⟂ₘ μ<GOAL>r • ν ⟂ₘ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h : μ ⟂ₘ ν<VAR>s : Set α<GOAL>μ.restrict s ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>h_ac : μ ≪ ν<VAR>h_ms : μ ⟂ₘ ν<GOAL>μ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>β : Type u_2<GOAL>∀ {x : MeasurableSpace β} {f : α → β}, MeasurableEmbedding f → μ ⟂ₘ ν → MeasureTheory.Measure.map f μ ⟂ₘ MeasureTheory.Measure.map f ν
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<GOAL>∑' (x : ↑s), 1 ≤ MeasureTheory.Measure.count s
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.Measure.count s = ∑' (i : ↑s), 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<GOAL>MeasureTheory.Measure.count ∅ = 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Finset α<VAR>s_mble : MeasurableSet ↑s<GOAL>MeasureTheory.Measure.count ↑s = ↑s.card
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Finset α<GOAL>MeasureTheory.Measure.count ↑s = ↑s.card
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>s_fin : s.Finite<VAR>s_mble : MeasurableSet s<GOAL>MeasureTheory.Measure.count s = ↑s_fin.toFinset.card
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>MeasureTheory.Measure.count s = ↑hs.toFinset.card
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>MeasureTheory.Measure.count s = ⊤
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>s_mble : MeasurableSet s<GOAL>MeasureTheory.Measure.count s = ⊤ ↔ s.Infinite
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>MeasurableSingletonClass α<GOAL>MeasureTheory.Measure.count s = ⊤ ↔ s.Infinite
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>s_mble : MeasurableSet s<GOAL>MeasureTheory.Measure.count s < ⊤ ↔ s.Finite
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>MeasurableSingletonClass α<GOAL>MeasureTheory.Measure.count s < ⊤ ↔ s.Finite
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>s_mble : MeasurableSet s<VAR>hsc : MeasureTheory.Measure.count s = 0<GOAL>s = ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>MeasurableSingletonClass α<VAR>hsc : MeasureTheory.Measure.count s = 0<GOAL>s = ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>s_mble : MeasurableSet s<GOAL>MeasureTheory.Measure.count s = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>MeasurableSingletonClass α<GOAL>MeasureTheory.Measure.count s = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>hs' : s.Nonempty<VAR>s_mble : MeasurableSet s<GOAL>MeasureTheory.Measure.count s ≠ 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : Set α<VAR>MeasurableSingletonClass α<VAR>hs' : s.Nonempty<GOAL>MeasureTheory.Measure.count s ≠ 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>a : α<VAR>ha : MeasurableSet {a}<GOAL>MeasureTheory.Measure.count {a} = 1
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<GOAL>MeasureTheory.Measure.count {a} = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>s : Set β<VAR>s_mble : MeasurableSet s<VAR>fs_mble : MeasurableSet (f '' s)<GOAL>MeasureTheory.Measure.count (f '' s) = MeasureTheory.Measure.count s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>MeasurableSingletonClass α<VAR>MeasurableSingletonClass β<VAR>f : β → α<VAR>hf : Function.Injective f<VAR>s : Set β<GOAL>MeasureTheory.Measure.count (f '' s) = MeasureTheory.Measure.count s
<GOAL>MeasureTheory.volume = StieltjesFunction.id.measure
<VAR>s : Set ℝ<GOAL>MeasureTheory.volume s = StieltjesFunction.id.measure s
<VAR>a b : ℝ<GOAL>MeasureTheory.volume (Set.Ico a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<GOAL>MeasureTheory.volume (Set.Icc a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<GOAL>MeasureTheory.volume (Set.Ioo a b) = ENNReal.ofReal (b - a)
<VAR>a b : ℝ<GOAL>MeasureTheory.volume (Set.Ioc a b) = ENNReal.ofReal (b - a)
<VAR>a : ℝ<GOAL>MeasureTheory.volume {a} = 0
<VAR>a r : ℝ<GOAL>MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal (2 * r)
<VAR>a r : ℝ<GOAL>MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal (2 * r)
<VAR>a : ℝ<VAR>r : ℝ≥0∞<GOAL>MeasureTheory.volume (EMetric.ball a r) = 2 * r
<VAR>a : ℝ<VAR>r : ℝ≥0∞<GOAL>MeasureTheory.volume (EMetric.closedBall a r) = 2 * r
<VAR>a b : ℝ<GOAL>MeasureTheory.volume (Set.uIcc a b) = ENNReal.ofReal |b - a|
<VAR>a : ℝ<GOAL>MeasureTheory.volume (Set.Ioi a) = ⊤
<VAR>a : ℝ<GOAL>MeasureTheory.volume (Set.Ici a) = ⊤
<VAR>a : ℝ<GOAL>MeasureTheory.volume (Set.Iio a) = ⊤
<VAR>a : ℝ<GOAL>MeasureTheory.volume (Set.Iic a) = ⊤
<VAR>s : Set ℝ<GOAL>MeasureTheory.volume s ≤ EMetric.diam s
<VAR>p : ℝ → Prop<VAR>a : ℝ<VAR>h : ∀ᶠ (x : ℝ) in 𝓝 a, p x<GOAL>0 < MeasureTheory.volume {x | p x}
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<GOAL>MeasureTheory.volume (Set.Icc a b) = ∏ i : ι, ENNReal.ofReal (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(MeasureTheory.volume (Set.Icc a b)).toReal = ∏ i : ι, (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<GOAL>MeasureTheory.volume (Set.univ.pi fun i => Set.Ioo (a i) (b i)) = ∏ i : ι, ENNReal.ofReal (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(MeasureTheory.volume (Set.univ.pi fun i => Set.Ioo (a i) (b i))).toReal = ∏ i : ι, (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<GOAL>MeasureTheory.volume (Set.univ.pi fun i => Set.Ioc (a i) (b i)) = ∏ i : ι, ENNReal.ofReal (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(MeasureTheory.volume (Set.univ.pi fun i => Set.Ioc (a i) (b i))).toReal = ∏ i : ι, (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<GOAL>MeasureTheory.volume (Set.univ.pi fun i => Set.Ico (a i) (b i)) = ∏ i : ι, ENNReal.ofReal (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a b : ι → ℝ<VAR>h : a ≤ b<GOAL>(MeasureTheory.volume (Set.univ.pi fun i => Set.Ico (a i) (b i))).toReal = ∏ i : ι, (b i - a i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>MeasureTheory.volume (Metric.ball a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>a : ι → ℝ<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>MeasureTheory.volume (Metric.closedBall a r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<GOAL>MeasureTheory.volume s ≤ ∏ i : ι, EMetric.diam (Function.eval i '' s)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>s : Set (ι → ℝ)<GOAL>MeasureTheory.volume s ≤ EMetric.diam s ^ Fintype.card ι
<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>ENNReal.ofReal |a| • MeasureTheory.Measure.map (fun x => a * x) MeasureTheory.volume = MeasureTheory.volume
<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>MeasureTheory.Measure.map (fun x => a * x) MeasureTheory.volume = ENNReal.ofReal |a⁻¹| • MeasureTheory.volume
<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>s : Set ℝ<GOAL>MeasureTheory.volume ((fun x => a * x) ⁻¹' s) = ENNReal.ofReal |a⁻¹| * MeasureTheory.volume s
<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>ENNReal.ofReal |a| • MeasureTheory.Measure.map (fun x => x * a) MeasureTheory.volume = MeasureTheory.volume
<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>MeasureTheory.Measure.map (fun x => x * a) MeasureTheory.volume = ENNReal.ofReal |a⁻¹| • MeasureTheory.volume
<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>s : Set ℝ<GOAL>MeasureTheory.volume ((fun x => x * a) ⁻¹' s) = ENNReal.ofReal |a⁻¹| * MeasureTheory.volume s
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>DecidableEq ι<VAR>D : ι → ℝ<VAR>h : (Matrix.diagonal D).det ≠ 0<GOAL>ENNReal.ofReal |(Matrix.diagonal D).det| • MeasureTheory.Measure.map (⇑(Matrix.toLin' (Matrix.diagonal D))) MeasureTheory.volume = MeasureTheory.volume
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>DecidableEq ι<VAR>t : Matrix.TransvectionStruct ι ℝ<GOAL>MeasureTheory.MeasurePreserving (⇑(Matrix.toLin' t.toMatrix)) MeasureTheory.volume MeasureTheory.volume
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>DecidableEq ι<VAR>M : Matrix ι ι ℝ<VAR>hM : M.det ≠ 0<GOAL>MeasureTheory.Measure.map (⇑(Matrix.toLin' M)) MeasureTheory.volume = ENNReal.ofReal |M.det⁻¹| • MeasureTheory.volume
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>f : (ι → ℝ) →ₗ[ℝ] ι → ℝ<VAR>hf : LinearMap.det f ≠ 0<GOAL>MeasureTheory.Measure.map (⇑f) MeasureTheory.volume = ENNReal.ofReal |(LinearMap.det f)⁻¹| • MeasureTheory.volume
<VAR>α : Type u_1<VAR>f g : α → ℝ<VAR>s : Set α<GOAL>regionBetween f g s ⊆ s ×ˢ Set.univ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (regionBetween f g s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ<VAR>hf : Measurable f<GOAL>MeasurableSet {p | p.2 = f p.1}
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>(μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y) ∂μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>MeasureTheory.SFinite μ<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hs : MeasurableSet s<GOAL>(μ.prod MeasureTheory.volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ENNReal.ofReal ((g - f) y) ∂μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioo (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ioc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : MeasureTheory.NullMeasurableSet s μ<GOAL>MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Set.Ioo a b), p x<GOAL>∀ᵐ (x : ℝ) ∂μ.restrict s, p x
<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>s : Set ℝ<VAR>p : ℝ → Prop<VAR>h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Set.Ioo a b → p x<GOAL>∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>‖↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>‖↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>h₀ : 0 ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>‖↑(MeasureTheory.SimpleFunc.approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : MeasureTheory.Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : MeasureTheory.eLpNorm (fun x => f x - y₀) p μ < ⊤<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) - f) p μ) Filter.atTop (𝓝 0)
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>BorelSpace E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>fmeas : Measurable f<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hi₀ : MeasureTheory.Memℒp (fun x => y₀) p μ<VAR>n : ℕ<GOAL>MeasureTheory.Memℒp (↑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) p μ
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>BorelSpace E<VAR>f : β → E<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : MeasureTheory.Measure β<VAR>fmeas : Measurable f<VAR>TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : MeasureTheory.eLpNorm f p μ < ⊤<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ) Filter.atTop (𝓝 0)
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>BorelSpace E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>fmeas : Measurable f<VAR>TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>n : ℕ<GOAL>MeasureTheory.Memℒp (↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n)) p μ
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>BorelSpace E<VAR>f : β → E<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>μ : MeasureTheory.Measure β<VAR>fmeas : Measurable f<VAR>TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>Filter.Tendsto (fun n => MeasureTheory.Memℒp.toLp ↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) Filter.atTop (𝓝 (MeasureTheory.Memℒp.toLp f hf))
<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, MeasureTheory.eLpNorm (f - ↑g) p μ < ε ∧ MeasureTheory.Memℒp (↑g) p μ
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>μ : MeasureTheory.Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : MeasureTheory.HasFiniteIntegral (fun x => f x - y₀) μ<GOAL>Filter.Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖₊ ∂μ) Filter.atTop (𝓝 0)
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>BorelSpace E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>fmeas : Measurable f<VAR>hf : MeasureTheory.Integrable f μ<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hi₀ : MeasureTheory.Integrable (fun x => y₀) μ<VAR>n : ℕ<GOAL>MeasureTheory.Integrable (↑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) μ
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>OpensMeasurableSpace E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})<VAR>fmeas : Measurable f<VAR>hf : MeasureTheory.Integrable f μ<GOAL>Filter.Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖₊ ∂μ) Filter.atTop (𝓝 0)
<VAR>β : Type u_2<VAR>E : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace E<VAR>NormedAddCommGroup E<VAR>BorelSpace E<VAR>f : β → E<VAR>μ : MeasureTheory.Measure β<VAR>fmeas : Measurable f<VAR>TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})<VAR>hf : MeasureTheory.Integrable f μ<VAR>n : ℕ<GOAL>MeasureTheory.Integrable (↑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n)) μ
<VAR>α : Type u_1<VAR>F : Type u_5<VAR>MeasurableSpace α<VAR>NormedAddCommGroup F<VAR>f : MeasureTheory.SimpleFunc α F<GOAL>∃ C, ∀ (x : α), ‖↑f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : MeasureTheory.SimpleFunc α E<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Memℒp (↑f) 0 μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : MeasureTheory.SimpleFunc α E<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Memℒp ↑f ⊤ μ
<VAR>α : Type u_1<VAR>F : Type u_5<VAR>MeasurableSpace α<VAR>NormedAddCommGroup F<VAR>p : ℝ<VAR>f : MeasureTheory.SimpleFunc α F<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.eLpNorm' (↑f) p μ = (∑ y ∈ f.range, ↑‖y‖₊ ^ p * μ (↑f ⁻¹' {y})) ^ (1 / p)