ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>(μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>(ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≤ μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>MeasureTheory.SFinite ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<GOAL>∫⁻ (x : α), μ.rnDeriv ν x ∂ν = μ Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<GOAL>MeasureTheory.IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) s ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SFinite ν<VAR>s : Set α<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν κ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<VAR>MeasureTheory.SigmaFinite κ<VAR>hμν : μ ≪ ν<GOAL>μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμν : μ ≤ ν<VAR>MeasureTheory.SigmaFinite ν<GOAL>μ.rnDeriv ν ≤ᵐ[ν] 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<GOAL>(fun x => (MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<GOAL>(fun x => (MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν) (f x)) =ᵐ[ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<GOAL>MeasureTheory.Measure.map f (ν.withDensity (μ.rnDeriv ν)) = (MeasureTheory.Measure.map f ν).withDensity ((MeasureTheory.Measure.map f μ).rnDeriv (MeasureTheory.Measure.map f ν))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : MeasurableEmbedding f<VAR>μ ν : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>MeasureTheory.SigmaFinite ν<GOAL>(MeasureTheory.Measure.map f μ).singularPart (MeasureTheory.Measure.map f ν) = MeasureTheory.Measure.map f (μ.singularPart ν)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>h : s ≪ᵥ μ.toENNRealVectorMeasure<GOAL>μ.withDensityᵥ (s.rnDeriv μ) = s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>s ≪ᵥ μ.toENNRealVectorMeasure ↔ μ.withDensityᵥ (s.rnDeriv μ) = s
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<GOAL>∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → E<GOAL>MeasureTheory.Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<GOAL>(ν.withDensityᵥ fun x => (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f
<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → E<GOAL>∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r : ℝ≥0∞<GOAL>HasFPowerSeriesWithinOnBall f p Set.univ x r ↔ HasFPowerSeriesOnBall f p x r
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x : E<GOAL>HasFPowerSeriesWithinAt f p Set.univ x ↔ HasFPowerSeriesAt f p x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>AnalyticWithinAt 𝕜 f Set.univ x ↔ AnalyticAt 𝕜 f x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>AnalyticWithinOn 𝕜 f Set.univ ↔ AnalyticOn 𝕜 f Set.univ
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>h : HasFPowerSeriesWithinAt f p s x<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : AnalyticWithinAt 𝕜 f s x<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : {x} ∈ 𝓝[s] x<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : AnalyticAt 𝕜 f x<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : AnalyticOn 𝕜 f s<GOAL>AnalyticWithinOn 𝕜 f s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : AnalyticWithinOn 𝕜 f s<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticWithinOn 𝕜 f (s ∩ u)<GOAL>AnalyticWithinOn 𝕜 f s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>AnalyticWithinOn 𝕜 f s ↔ AnalyticOn 𝕜 f s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ≥0∞<GOAL>HasFPowerSeriesWithinOnBall f p s x r ↔ ContinuousWithinAt f s x ∧ ∃ g, Set.EqOn f g (s ∩ EMetric.ball x r) ∧ HasFPowerSeriesOnBall g p x r
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>x : E<GOAL>HasFPowerSeriesWithinAt f p s x ↔ ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ HasFPowerSeriesAt g p x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>AnalyticWithinAt 𝕜 f s x ↔ ContinuousWithinAt f s x ∧ ∃ g, f =ᶠ[𝓝[s] x] g ∧ AnalyticAt 𝕜 g x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : AnalyticWithinAt 𝕜 f s x<GOAL>∃ g, f x = g x ∧ f =ᶠ[𝓝[s] x] g ∧ AnalyticAt 𝕜 g x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<GOAL>AnalyticWithinAt 𝕜 g s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s x<VAR>hs : Set.EqOn f g s<VAR>hx : f x = g x<GOAL>AnalyticWithinAt 𝕜 g s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f g : E → F<VAR>s : Set E<VAR>hf : AnalyticWithinOn 𝕜 f s<VAR>hs : Set.EqOn f g s<GOAL>AnalyticWithinOn 𝕜 g s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s t : Set E<VAR>x : E<VAR>r : ℝ≥0∞<VAR>h : HasFPowerSeriesWithinOnBall f p t x r<VAR>hs : s ⊆ t<GOAL>HasFPowerSeriesWithinOnBall f p s x r
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s t : Set E<VAR>x : E<VAR>h : HasFPowerSeriesWithinAt f p t x<VAR>hs : s ⊆ t<GOAL>HasFPowerSeriesWithinAt f p s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s t : Set E<VAR>x : E<VAR>h : AnalyticWithinAt 𝕜 f t x<VAR>hs : s ⊆ t<GOAL>AnalyticWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s t : Set E<VAR>h : AnalyticWithinOn 𝕜 f t<VAR>hs : s ⊆ t<GOAL>AnalyticWithinOn 𝕜 f s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace F<VAR>CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>x : E<VAR>hf : AnalyticWithinAt 𝕜 f s (g x)<VAR>hg : AnalyticWithinAt 𝕜 g t x<VAR>h : Set.MapsTo g t s<GOAL>AnalyticWithinAt 𝕜 (f ∘ g) t x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace F<VAR>CompleteSpace G<VAR>f : F → G<VAR>g : E → F<VAR>s : Set F<VAR>t : Set E<VAR>hf : AnalyticWithinOn 𝕜 f s<VAR>hg : AnalyticWithinOn 𝕜 g t<VAR>h : Set.MapsTo g t s<GOAL>AnalyticWithinOn 𝕜 (f ∘ g) t
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : AnalyticWithinAt 𝕜 f s x<VAR>n : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>h : AnalyticWithinOn 𝕜 f s<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>r t : ℝ≥0∞<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinOnBall f p s e r<VAR>hg : HasFPowerSeriesWithinOnBall g q s e t<GOAL>HasFPowerSeriesWithinOnBall (fun x => (f x, g x)) (p.prod q) s e (min r t)
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>hf : HasFPowerSeriesWithinAt f p s e<VAR>hg : HasFPowerSeriesWithinAt g q s e<GOAL>HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>hf : AnalyticWithinAt 𝕜 f s e<VAR>hg : AnalyticWithinAt 𝕜 g s e<GOAL>AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e
<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>hf : AnalyticWithinOn 𝕜 f s<VAR>hg : AnalyticWithinOn 𝕜 g s<GOAL>AnalyticWithinOn 𝕜 (fun x => (f x, g x)) s
<VAR>ι : Type u_1<VAR>Fintype ι<GOAL>(Pi.basisFun ℝ ι).parallelepiped = TopologicalSpace.PositiveCompacts.piIcc01 ι
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<GOAL>b.parallelepiped = TopologicalSpace.PositiveCompacts.map ⇑b.equivFun.symm ⋯ ⋯ (TopologicalSpace.PositiveCompacts.piIcc01 ι)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>MeasurableSpace E<VAR>MeasurableSpace F<VAR>BorelSpace E<VAR>BorelSpace F<VAR>SecondCountableTopology F<VAR>SigmaCompactSpace F<VAR>b : Basis ι ℝ E<VAR>f : E ≃L[ℝ] F<GOAL>MeasureTheory.Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar
<GOAL>MeasureTheory.Measure.addHaarMeasure TopologicalSpace.PositiveCompacts.Icc01 = MeasureTheory.volume
<VAR>ι : Type u_1<VAR>Fintype ι<GOAL>MeasureTheory.Measure.addHaarMeasure (TopologicalSpace.PositiveCompacts.piIcc01 ι) = MeasureTheory.volume
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>sb : Bornology.IsBounded s<VAR>hu : Bornology.IsBounded (Set.range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<GOAL>μ s = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>u : ℕ → E<VAR>hu : Bornology.IsBounded (Set.range u)<VAR>hs : Pairwise (Disjoint on fun n => {u n} + s)<VAR>h's : MeasurableSet s<GOAL>μ s = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Submodule ℝ E<VAR>hs : s ≠ ⊤<GOAL>μ ↑s = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : AffineSubspace ℝ E<VAR>hs : s ≠ ⊤<GOAL>μ ↑s = 0
<VAR>ι : Type u_1<VAR>Finite ι<VAR>f : (ι → ℝ) →ₗ[ℝ] ι → ℝ<VAR>hf : LinearMap.det f ≠ 0<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>μ.IsAddHaarMeasure<GOAL>MeasureTheory.Measure.map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →ₗ[ℝ] E<VAR>hf : LinearMap.det f ≠ 0<GOAL>MeasureTheory.Measure.map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →ₗ[ℝ] E<VAR>hf : LinearMap.det f ≠ 0<VAR>s : Set E<GOAL>μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →L[ℝ] E<VAR>hf : LinearMap.det ↑f ≠ 0<VAR>s : Set E<GOAL>μ (⇑f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det ↑f)⁻¹| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E ≃ₗ[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E ≃L[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑↑f.symm| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →ₗ[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →L[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑f| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E ≃L[ℝ] E<VAR>s : Set E<GOAL>μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det ↑↑f| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →ₗ[ℝ] E<VAR>hf : LinearMap.det f ≠ 0<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (⇑f) μ μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>f : E →L[ℝ] E<VAR>hf : f.det ≠ 0<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (⇑f) μ μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>MeasureTheory.Measure.map (fun x => r • x) μ = ENNReal.ofReal |(r ^ FiniteDimensional.finrank ℝ E)⁻¹| • μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>MeasureTheory.Measure.QuasiMeasurePreserving (fun x => r • x) μ μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hr : r ≠ 0<VAR>s : Set E<GOAL>μ ((fun x => r • x) ⁻¹' s) = ENNReal.ofReal |(r ^ FiniteDimensional.finrank ℝ E)⁻¹| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>s : Set E<GOAL>μ (r • s) = ENNReal.ofReal |r ^ FiniteDimensional.finrank ℝ E| * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>s : Set E<GOAL>μ (r • s) = ENNReal.ofReal (r ^ FiniteDimensional.finrank ℝ E) * μ s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>s : Set E<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>r : ℝ<GOAL>MeasureTheory.NullMeasurableSet (r • s) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>x : E<VAR>r : ℝ<VAR>s : Set E<GOAL>μ (⇑(AffineMap.homothety x r) '' s) = ENNReal.ofReal |r ^ FiniteDimensional.finrank ℝ E| * μ s