ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>g : α → β<VAR>γ : Type u_5<GOAL>∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ}, MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) → AEMeasurable f μ → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>g : α → β<VAR>γ : Type u_5<GOAL>∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ}, MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) → Measurable f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>g : α → β<VAR>γ : Type u_5<GOAL>∀ {x : MeasurableSpace γ} {x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α}, MeasureTheory.AEStronglyMeasurable g ν → MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<GOAL>MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable f μ ∧ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace β<VAR>BorelSpace β<GOAL>MeasureTheory.AEStronglyMeasurable f μ ↔ MeasureTheory.NullMeasurable f μ ∧ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mα : MeasurableSpace α<VAR>f : γ → α<VAR>μ : MeasureTheory.Measure γ<VAR>hf : MeasurableEmbedding f<VAR>g : α → β<GOAL>MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Embedding g<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => g (f x)) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>ι : Type u_5<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>u : Filter ι<VAR>u.NeBot<VAR>u.IsCountablyGenerated<VAR>f : ι → α → β<VAR>g : α → β<VAR>hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (𝓝 (g x))<GOAL>MeasureTheory.AEStronglyMeasurable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f : ℕ → α → β<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 l)<GOAL>∃ f_lim, MeasureTheory.StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)<VAR>hg : MeasureTheory.AEStronglyMeasurable g (μ.restrict sᶜ)<GOAL>MeasureTheory.AEStronglyMeasurable (s.piecewise f g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>Countable ι<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>m : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<VAR>h : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ i)<GOAL>MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.sum μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>Countable ι<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>_m : MeasurableSpace α<VAR>μ : ι → MeasureTheory.Measure α<GOAL>MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>ν : MeasureTheory.Measure α<GOAL>MeasureTheory.AEStronglyMeasurable f (μ + ν) ↔ MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.AEStronglyMeasurable f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>ν : MeasureTheory.Measure α<VAR>f : α → β<VAR>hμ : MeasureTheory.AEStronglyMeasurable f μ<VAR>hν : MeasureTheory.AEStronglyMeasurable f ν<GOAL>MeasureTheory.AEStronglyMeasurable f (μ + ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>Countable ι<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ i, s i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_4<VAR>Countable ι<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>s : ι → Set α<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict (⋃ i, s i)) ↔ ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (s i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>s t : Set α<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict (s ∪ t)) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s) ∧ MeasureTheory.AEStronglyMeasurable f (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>LinearOrder α<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>f : α → β<VAR>a b : α<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b)) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b)) ∧ MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>R : Type u_5<VAR>Monoid R<VAR>DistribMulAction R ℝ≥0∞<VAR>IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>h : MeasureTheory.AEStronglyMeasurable f μ<VAR>c : R<GOAL>MeasureTheory.AEStronglyMeasurable f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>G : Type u_6<VAR>Group G<VAR>MulAction G β<VAR>ContinuousConstSMul G β<VAR>c : G<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>M : Type u_5<VAR>Monoid M<VAR>MulAction M β<VAR>ContinuousConstSMul M β<VAR>c : M<VAR>hc : IsUnit c<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>G₀ : Type u_7<VAR>GroupWithZero G₀<VAR>MulAction G₀ β<VAR>ContinuousConstSMul G₀ β<VAR>c : G₀<VAR>hc : c ≠ 0<GOAL>MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>MeasureTheory.FinStronglyMeasurable (MeasureTheory.AEFinStronglyMeasurable.mk f hf) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>f =ᵐ[μ] MeasureTheory.AEFinStronglyMeasurable.mk f hf
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>Zero β<VAR>MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>f : α → β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>MonoidWithZero β<VAR>ContinuousMul β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEFinStronglyMeasurable g μ<GOAL>MeasureTheory.AEFinStronglyMeasurable (f * g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEFinStronglyMeasurable g μ<GOAL>MeasureTheory.AEFinStronglyMeasurable (f + g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>MeasureTheory.AEFinStronglyMeasurable (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>AddGroup β<VAR>ContinuousSub β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEFinStronglyMeasurable g μ<GOAL>MeasureTheory.AEFinStronglyMeasurable (f - g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>AddMonoid β<VAR>Monoid 𝕜<VAR>DistribMulAction 𝕜 β<VAR>ContinuousSMul 𝕜 β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.AEFinStronglyMeasurable (c • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>Zero β<VAR>SemilatticeSup β<VAR>ContinuousSup β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEFinStronglyMeasurable g μ<GOAL>MeasureTheory.AEFinStronglyMeasurable (f ⊔ g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>Zero β<VAR>SemilatticeInf β<VAR>ContinuousInf β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEFinStronglyMeasurable g μ<GOAL>MeasureTheory.AEFinStronglyMeasurable (f ⊓ g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>T2Space β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ MeasureTheory.SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>T2Space β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>MeasurableSet hf.sigmaFiniteSet
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>Zero β<VAR>T2Space β<VAR>hf : MeasureTheory.AEFinStronglyMeasurable f μ<GOAL>f =ᵐ[μ.restrict hf.sigmaFiniteSetᶜ] 0
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>SeminormedAddCommGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>f : α → G<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>MeasureTheory.FinStronglyMeasurable f μ ↔ Measurable f
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>SeminormedAddCommGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>f : α → G<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>hf : Measurable f<GOAL>MeasureTheory.FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>SeminormedAddCommGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>f : α → G<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<GOAL>MeasureTheory.AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>SeminormedAddCommGroup G<VAR>MeasurableSpace G<VAR>BorelSpace G<VAR>SecondCountableTopology G<VAR>f : α → G<VAR>_m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.AEFinStronglyMeasurable f μ
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>TopologicalSpace ι<VAR>TopologicalSpace.MetrizableSpace ι<VAR>MeasurableSpace ι<VAR>SecondCountableTopology ι<VAR>OpensMeasurableSpace ι<VAR>mβ : MeasurableSpace β<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>BorelSpace β<VAR>m : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), Measurable (u i)<GOAL>Measurable (Function.uncurry u)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>TopologicalSpace ι<VAR>TopologicalSpace.MetrizableSpace ι<VAR>MeasurableSpace ι<VAR>SecondCountableTopology ι<VAR>OpensMeasurableSpace ι<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)<GOAL>MeasureTheory.StronglyMeasurable (Function.uncurry u)
<VAR>a : ℂ<GOAL>Complex.measurableEquivPi a = ![a.re, a.im]
<VAR>p : Fin 2 → ℝ<GOAL>Complex.measurableEquivPi.symm p = ↑(p 0) + ↑(p 1) * Complex.I
<VAR>a : ℂ<GOAL>Complex.measurableEquivRealProd a = (a.re, a.im)
<VAR>p : ℝ × ℝ<GOAL>Complex.measurableEquivRealProd.symm p = { re := p.1, im := p.2 }
<GOAL>MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivPi) MeasureTheory.volume MeasureTheory.volume
<GOAL>MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivRealProd) MeasureTheory.volume MeasureTheory.volume
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.AddContent C<VAR>I : Finset (Set α)<VAR>_h_ss : ↑I ⊆ C<VAR>_h_dis : (↑I).PairwiseDisjoint id<VAR>_h_mem : ⋃₀ ↑I ∈ C<GOAL>self.toFun (⋃₀ ↑I) = ∑ u ∈ I, self.toFun u
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>self : MeasureTheory.AddContent C<GOAL>self.toFun ∅ = 0
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>m m' : MeasureTheory.AddContent C<VAR>h : ∀ (s : Set α), m s = m' s<GOAL>m = m'
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>m m' : MeasureTheory.AddContent C<GOAL>m = m' ↔ ∀ (s : Set α), m s = m' s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>m : MeasureTheory.AddContent C<GOAL>m ∅ = 0
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>I : Finset (Set α)<VAR>m : MeasureTheory.AddContent C<VAR>h_ss : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<VAR>h_mem : ⋃₀ ↑I ∈ C<GOAL>m (⋃₀ ↑I) = ∑ u ∈ I, m u
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>m : MeasureTheory.AddContent C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ∪ t ∈ C<VAR>h_dis : Disjoint s t<GOAL>m (s ∪ t) = m s + m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s : Set α<VAR>I : Finset (Set α)<VAR>m : MeasureTheory.AddContent C<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<VAR>h_dis : (↑I).PairwiseDisjoint id<GOAL>m s = ∑ i ∈ I, m i + ∑ i ∈ hC.diffFinset₀ hs hI, m i
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>t : Set α<VAR>I : Finset (Set α)<VAR>m : MeasureTheory.AddContent C<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>h_ss : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<VAR>ht : t ∈ C<VAR>hJt : ∀ s ∈ I, s ⊆ t<GOAL>∑ u ∈ I, m u ≤ m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>m : MeasureTheory.AddContent C<VAR>hC : MeasureTheory.IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ⊆ t<GOAL>m s ≤ m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>m : MeasureTheory.AddContent C<VAR>hC : MeasureTheory.IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>h_dis : Disjoint s t<GOAL>m (s ∪ t) = m s + m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>m : MeasureTheory.AddContent C<VAR>hC : MeasureTheory.IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m (s ∪ t) ≤ m s + m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>m : MeasureTheory.AddContent C<VAR>ι : Type u_2<VAR>hC : MeasureTheory.IsSetRing C<VAR>s : ι → Set α<VAR>S : Finset ι<VAR>hs : ∀ n ∈ S, s n ∈ C<GOAL>m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>m : MeasureTheory.AddContent C<VAR>hC : MeasureTheory.IsSetRing C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>m s - m t ≤ m (s \ t)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α ℂ<GOAL>MeasureTheory.ComplexMeasure.re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>v : MeasureTheory.VectorMeasure α ℂ<GOAL>MeasureTheory.ComplexMeasure.im v = v.mapRange Complex.imLm.toAddMonoidHom Complex.continuous_im
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>i : Set α<GOAL>(↑(s.toComplexMeasure t) i).im = ↑t i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>i : Set α<GOAL>(↑(s.toComplexMeasure t) i).re = ↑s i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<VAR>i : Set α<GOAL>↑(s.toComplexMeasure t) i = { re := ↑s i, im := ↑t i }
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>c : MeasureTheory.ComplexMeasure α<GOAL>(MeasureTheory.ComplexMeasure.re c).toComplexMeasure (MeasureTheory.ComplexMeasure.im c) = c
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<GOAL>MeasureTheory.ComplexMeasure.re (s.toComplexMeasure t) = s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>s t : MeasureTheory.SignedMeasure α<GOAL>MeasureTheory.ComplexMeasure.im (s.toComplexMeasure t) = t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>c : MeasureTheory.ComplexMeasure α<GOAL>MeasureTheory.ComplexMeasure.equivSignedMeasure c = (MeasureTheory.ComplexMeasure.re c, MeasureTheory.ComplexMeasure.im c)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<GOAL>∀ (x : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α), MeasureTheory.ComplexMeasure.equivSignedMeasure.symm x = match x with | (s, t) => s.toComplexMeasure t
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R ℝ<VAR>ContinuousConstSMul R ℝ<VAR>ContinuousConstSMul R ℂ<GOAL>∀ (a : MeasureTheory.SignedMeasure α × MeasureTheory.SignedMeasure α), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ.symm a = MeasureTheory.ComplexMeasure.equivSignedMeasure.invFun a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R ℝ<VAR>ContinuousConstSMul R ℝ<VAR>ContinuousConstSMul R ℂ<GOAL>∀ (a : MeasureTheory.ComplexMeasure α), MeasureTheory.ComplexMeasure.equivSignedMeasureₗ a = MeasureTheory.ComplexMeasure.equivSignedMeasure.toFun a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>c : MeasureTheory.ComplexMeasure α<VAR>μ : MeasureTheory.VectorMeasure α ℝ≥0∞<GOAL>c ≪ᵥ μ ↔ MeasureTheory.ComplexMeasure.re c ≪ᵥ μ ∧ MeasureTheory.ComplexMeasure.im c ≪ᵥ μ
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>v : ι → E<VAR>x : E<GOAL>x ∈ parallelepiped v ↔ ∃ t ∈ Set.Icc 0 1, x = ∑ i : ι, t i • v i
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>b : Basis ι ℝ E<GOAL>parallelepiped ⇑b = {x | ∀ (i : ι), (b.repr x) i ∈ Set.Icc 0 1}
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Fintype ι<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>f : E →ₗ[ℝ] F<VAR>v : ι → E<GOAL>⇑f '' parallelepiped v = parallelepiped (⇑f ∘ v)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>Fintype ι<VAR>Fintype ι'<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>v : ι → E<VAR>e : ι' ≃ ι<GOAL>parallelepiped (v ∘ ⇑e) = parallelepiped v
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>b : OrthonormalBasis ι ℝ ℝ<GOAL>parallelepiped ⇑b = Set.Icc 0 1 ∨ parallelepiped ⇑b = Set.Icc (-1) 0
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>v : ι → E<GOAL>parallelepiped v = ∑ i : ι, segment ℝ 0 (v i)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>v : ι → E<GOAL>Convex ℝ (parallelepiped v)
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>v : ι → E<GOAL>parallelepiped v = (convexHull ℝ) (∑ i : ι, {0, v i})
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>DecidableEq ι<VAR>a : ι → ℝ<GOAL>(parallelepiped fun i => Pi.single i (a i)) = Set.uIcc 0 a
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<GOAL>↑b.parallelepiped = parallelepiped ⇑b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>Fintype ι<VAR>Fintype ι'<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).parallelepiped = b.parallelepiped
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>b : Basis ι ℝ E<VAR>e : E ≃ₗ[ℝ] F<GOAL>(b.map e).parallelepiped = TopologicalSpace.PositiveCompacts.map ⇑e ⋯ ⋯ b.parallelepiped
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Fintype ι<VAR>Fintype ι'<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<GOAL>(v.prod w).parallelepiped = v.parallelepiped.prod w.parallelepiped
<VAR>ι : Type u_5<VAR>E : Type u_6<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>b : Basis ι ℝ E<GOAL>b.addHaar = MeasureTheory.Measure.addHaarMeasure b.parallelepiped
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>SecondCountableTopology E<VAR>b : Basis ι ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>MeasureTheory.SigmaFinite μ<VAR>μ.IsAddLeftInvariant<GOAL>b.addHaar = μ ↔ μ ↑b.parallelepiped = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>Fintype ι<VAR>Fintype ι'<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>b : Basis ι ℝ E<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).addHaar = b.addHaar
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>Fintype ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>b : Basis ι ℝ E<GOAL>b.addHaar (parallelepiped ⇑b) = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Fintype ι<VAR>Fintype ι'<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ E<VAR>NormedSpace ℝ F<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>MeasurableSpace F<VAR>BorelSpace F<VAR>SecondCountableTopologyEither E F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<GOAL>(v.prod w).addHaar = v.addHaar.prod w.addHaar
<VAR>ι : Type u_1<GOAL>(EuclideanSpace.measurableEquiv ι).toEquiv = WithLp.equiv 2 ((i : ι) → (fun x => ℝ) i)
<VAR>ι : Type u_1<GOAL>⇑(EuclideanSpace.measurableEquiv ι) = ⇑(WithLp.equiv 2 ((i : ι) → (fun x => ℝ) i))
<VAR>ι : Type u_1<GOAL>⇑(EuclideanSpace.measurableEquiv ι).symm = ⇑(WithLp.equiv 2 (ι → ℝ)).symm
<VAR>G : Type u_1<VAR>Group G<VAR>V : Set G<GOAL>MeasureTheory.Measure.haar.index ∅ V = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>V : Set G<GOAL>MeasureTheory.Measure.haar.addIndex ∅ V = 0
<VAR>G : Type u_1<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>K₀ : TopologicalSpace.PositiveCompacts G<VAR>U : Set G<GOAL>MeasureTheory.Measure.haar.addPrehaar (↑K₀) U ⊥ = 0