ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<VAR>f : B ⟶ (CategoryTheory.ihom A).obj C<GOAL>((Rep.MonoidalClosed.linearHomEquiv A B C).symm f).hom = (TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) (LinearMap.flip f.hom)
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A B C : Rep k G<VAR>f : A ⟶ (CategoryTheory.ihom B).obj C<GOAL>((Rep.MonoidalClosed.linearHomEquivComm A B C).symm f).hom = (TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe B) (CoeSort.coe C)) f.hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V W : Type u<VAR>AddCommGroup V<VAR>AddCommGroup W<VAR>Module k V<VAR>Module k W<VAR>ρ : Representation k G V<VAR>τ : Representation k G W<VAR>x : TensorProduct k V W<GOAL>(ρ.repOfTprodIso τ).hom.hom x = x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V W : Type u<VAR>AddCommGroup V<VAR>AddCommGroup W<VAR>Module k V<VAR>Module k W<VAR>ρ : Representation k G V<VAR>τ : Representation k G W<VAR>x : TensorProduct k V W<GOAL>(ρ.repOfTprodIso τ).inv.hom x = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>CommRing k<VAR>Monoid G<VAR>V : Type u_3<VAR>W : Type u_4<VAR>AddCommGroup V<VAR>AddCommGroup W<VAR>Module k V<VAR>Module k W<VAR>ρ : G →* V →ₗ[k] V<VAR>σ : G →* W →ₗ[k] W<VAR>f : V →ₗ[k] W<VAR>w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f<VAR>r : MonoidAlgebra k G<VAR>x : V<GOAL>f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>M : ModuleCat (MonoidAlgebra k G)<GOAL>CoeSort.coe (Rep.ofModuleMonoidAlgebra.obj M) = RestrictScalars k (MonoidAlgebra k G) ↑M
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>M : ModuleCat (MonoidAlgebra k G)<GOAL>(Rep.ofModuleMonoidAlgebra.obj M).ρ = Representation.ofModule ↑M
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>V : Rep k G<VAR>g : G<VAR>x : CoeSort.coe V<GOAL>Rep.unitIsoAddEquiv ((V.ρ g).toFun x) = ((Rep.ofModuleMonoidAlgebra.obj (Rep.toModuleMonoidAlgebra.obj V)).ρ g).toFun (Rep.unitIsoAddEquiv x)
<VAR>n : ℕ<VAR>c : Fin n → ℂ<VAR>R θ : Fin n → ℝ<GOAL>torusMap c R θ - c = torusMap 0 R θ
<VAR>n : ℕ<VAR>c : Fin n → ℂ<VAR>R θ : Fin n → ℝ<GOAL>torusMap c R θ = c ↔ R = 0
<VAR>n : ℕ<VAR>c : Fin n → ℂ<GOAL>torusMap c 0 = Function.const (Fin n → ℝ) c
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>a : E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>TorusIntegrable (fun x => a) c R
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>hf : TorusIntegrable f c R<GOAL>TorusIntegrable (-f) c R
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>hf : TorusIntegrable f c R<VAR>hg : TorusIntegrable g c R<GOAL>TorusIntegrable (f + g) c R
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>hf : TorusIntegrable f c R<VAR>hg : TorusIntegrable g c R<GOAL>TorusIntegrable (f - g) c R
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<GOAL>TorusIntegrable f c 0
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>NormedSpace ℂ E<VAR>hf : TorusIntegrable f c R<GOAL>MeasureTheory.IntegrableOn (fun θ => (∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * Complex.I) * Complex.I) • f (torusMap c R θ)) (Set.Icc 0 fun x => 2 * π) MeasureTheory.volume
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>hn : n ≠ 0<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<GOAL>(∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), -f x) = -∯ (x : Fin n → ℂ) in T(c, R), f x
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>hf : TorusIntegrable f c R<VAR>hg : TorusIntegrable g c R<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), f x + g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) + ∯ (x : Fin n → ℂ) in T(c, R), g x
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>hf : TorusIntegrable f c R<VAR>hg : TorusIntegrable g c R<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), f x - g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) - ∯ (x : Fin n → ℂ) in T(c, R), g x
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass 𝕜 ℂ E<VAR>a : 𝕜<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), a • f x) = a • ∯ (x : Fin n → ℂ) in T(c, R), f x
<VAR>n : ℕ<VAR>a : ℂ<VAR>f : (Fin n → ℂ) → ℂ<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>(∯ (x : Fin n → ℂ) in T(c, R), a * f x) = a * ∯ (x : Fin n → ℂ) in T(c, R), f x
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>C : ℝ<VAR>hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C<GOAL>‖∯ (x : Fin n → ℂ) in T(c, R), f x‖ ≤ ((2 * π) ^ n * ∏ i : Fin n, |R i|) * C
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>CompleteSpace E<VAR>f : (Fin 0 → ℂ) → E<VAR>c : Fin 0 → ℂ<VAR>R : Fin 0 → ℝ<GOAL>(∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : (Fin 1 → ℂ) → E<VAR>c : Fin 1 → ℂ<VAR>R : Fin 1 → ℝ<GOAL>(∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<VAR>i : Fin (n + 1)<GOAL>(∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)
<VAR>n : ℕ<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<GOAL>(∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>MeasurableSpace α<VAR>MeasurableSup α<GOAL>Measurable oneLePart
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>MeasurableSpace α<VAR>MeasurableSup α<GOAL>Measurable posPart
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>AddGroup α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>MeasurableSup α<GOAL>Measurable fun x => (f x)⁺
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Group α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>MeasurableSup α<GOAL>Measurable fun x => (f x)⁺ᵐ
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>MeasurableSpace α<VAR>MeasurableSup α<VAR>MeasurableNeg α<GOAL>Measurable negPart
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>MeasurableSpace α<VAR>MeasurableSup α<VAR>MeasurableInv α<GOAL>Measurable leOnePart
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Group α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>MeasurableSup α<VAR>MeasurableInv α<GOAL>Measurable fun x => (f x)⁻ᵐ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>AddGroup α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>MeasurableSup α<VAR>MeasurableNeg α<GOAL>Measurable fun x => (f x)⁻
<VAR>α : Type u_1<VAR>Lattice α<VAR>AddGroup α<VAR>MeasurableSpace α<VAR>MeasurableNeg α<VAR>MeasurableSup₂ α<GOAL>Measurable abs
<VAR>α : Type u_1<VAR>Lattice α<VAR>Group α<VAR>MeasurableSpace α<VAR>MeasurableInv α<VAR>MeasurableSup₂ α<GOAL>Measurable mabs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>Group α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>MeasurableInv α<VAR>MeasurableSup₂ α<GOAL>Measurable fun x => mabs (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Lattice α<VAR>AddGroup α<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>f : β → α<VAR>hf : Measurable f<VAR>MeasurableNeg α<VAR>MeasurableSup₂ α<GOAL>Measurable fun x => |f x|
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>Sup M<VAR>self : MeasurableSup M<VAR>c : M<GOAL>Measurable fun x => c ⊔ x
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>Sup M<VAR>self : MeasurableSup M<VAR>c : M<GOAL>Measurable fun x => x ⊔ c
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>Sup M<VAR>self : MeasurableSup₂ M<GOAL>Measurable fun p => p.1 ⊔ p.2
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>Inf M<VAR>self : MeasurableInf M<VAR>c : M<GOAL>Measurable fun x => c ⊓ x
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>Inf M<VAR>self : MeasurableInf M<VAR>c : M<GOAL>Measurable fun x => x ⊓ c
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>Inf M<VAR>self : MeasurableInf₂ M<GOAL>Measurable fun p => p.1 ⊓ p.2
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>Sup M<VAR>MeasurableSup M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => c ⊔ f x
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → M<VAR>Sup M<VAR>MeasurableSup M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => c ⊔ f x) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>Sup M<VAR>MeasurableSup M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => f x ⊔ c
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → M<VAR>Sup M<VAR>MeasurableSup M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => f x ⊔ c) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>Sup M<VAR>MeasurableSup₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (f ⊔ g)
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>Sup M<VAR>MeasurableSup₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => f a ⊔ g a
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → M<VAR>Sup M<VAR>MeasurableSup₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (f ⊔ g) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → M<VAR>Sup M<VAR>MeasurableSup₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => f a ⊔ g a) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>Inf M<VAR>MeasurableInf M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => c ⊓ f x
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → M<VAR>Inf M<VAR>MeasurableInf M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => c ⊓ f x) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>Inf M<VAR>MeasurableInf M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => f x ⊓ c
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → M<VAR>Inf M<VAR>MeasurableInf M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => f x ⊓ c) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>Inf M<VAR>MeasurableInf₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (f ⊓ g)
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>Inf M<VAR>MeasurableInf₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => f a ⊓ g a
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → M<VAR>Inf M<VAR>MeasurableInf₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (f ⊓ g) μ
<VAR>M : Type u_1<VAR>MeasurableSpace M<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → M<VAR>Inf M<VAR>MeasurableInf₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => f a ⊓ g a) μ
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>δ : Type u_3<VAR>MeasurableSpace δ<VAR>SemilatticeSup α<VAR>MeasurableSup₂ α<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>f : ι → δ → α<VAR>hf : ∀ n ∈ s, Measurable (f n)<GOAL>Measurable (s.sup' hs f)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>δ : Type u_3<VAR>MeasurableSpace δ<VAR>SemilatticeSup α<VAR>MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Measurable (f k)<GOAL>Measurable ((Finset.range (n + 1)).sup' ⋯ f)
<VAR>α : Type u_2<VAR>m : MeasurableSpace α<VAR>δ : Type u_3<VAR>MeasurableSpace δ<VAR>SemilatticeSup α<VAR>MeasurableSup₂ α<VAR>f : ℕ → δ → α<VAR>n : ℕ<VAR>hf : ∀ k ≤ n, Measurable (f k)<GOAL>Measurable fun x => (Finset.range (n + 1)).sup' ⋯ fun k => f k x
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<VAR>Finite α<GOAL>∃ n, Nonempty (α ≃ᵐ ↑(Set.range fun x => ↑↑x))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<VAR>Infinite α<VAR>Countable α<GOAL>Nonempty (α ≃ᵐ ↑(Set.range Nat.cast))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<GOAL>∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>StandardBorelSpace α<GOAL>∃ f, MeasurableEmbedding f
<VAR>Ω : Type u_2<VAR>MeasurableSpace Ω<VAR>StandardBorelSpace Ω<GOAL>MeasurableEmbedding (MeasureTheory.embeddingReal Ω)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>EventuallyMeasurableSet m l s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<GOAL>m ≤ EventuallyMeasurableSpace m l
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>s : Set α<VAR>hs : s ∈ l<GOAL>EventuallyMeasurableSet m l s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>s t : Set α<VAR>ht : EventuallyMeasurableSet m l t<VAR>hst : s =ᶠ[l] t<GOAL>EventuallyMeasurableSet m l s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<GOAL>EventuallyMeasurable m l f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>f : α → β<VAR>h : β → γ<VAR>hh : Measurable h<VAR>hf : EventuallyMeasurable m l f<GOAL>EventuallyMeasurable m l (h ∘ f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f g : α → β<VAR>hf : EventuallyMeasurable m l f<VAR>hgf : g =ᶠ[l] f<GOAL>EventuallyMeasurable m l g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>l : Filter α<VAR>CountableInterFilter l<VAR>β : Type u_2<VAR>MeasurableSpace β<VAR>f g : α → β<VAR>hf : Measurable f<VAR>hgf : g =ᶠ[l] f<GOAL>EventuallyMeasurable m l g
<VAR>a : ℝ<GOAL>Measurable QuotientAddGroup.mk
<VAR>T : ℝ<VAR>hT : 0 < T<VAR>t : ℝ<VAR>μ : MeasureTheory.Measure ℝ := by volume_tac<GOAL>MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T)) (Set.Ioc t (t + T)) μ
<VAR>T : ℝ<VAR>hT : 0 < T<VAR>t : ℝ<VAR>μ : MeasureTheory.Measure ℝ := by volume_tac<GOAL>MeasureTheory.IsAddFundamentalDomain (↥(AddSubgroup.zmultiples T).op) (Set.Ioc t (t + T)) μ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>MeasureTheory.volume Set.univ = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<GOAL>MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + T))) MeasureTheory.volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>U : Set (AddCircle T)<VAR>meas_U : MeasurableSet U<GOAL>MeasureTheory.volume U = MeasureTheory.volume (QuotientAddGroup.mk ⁻¹' U ∩ Set.Ioc t (t + T))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<GOAL>MeasureTheory.volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>t : ℝ<VAR>f : AddCircle T → ℝ≥0∞<GOAL>∫⁻ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : ℝ<VAR>f : AddCircle T → E<GOAL>∫ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : ℝ<VAR>f : AddCircle T → E<GOAL>∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b
<VAR>t : ℝ<GOAL>MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + 1))) MeasureTheory.volume
<VAR>t : ℝ<VAR>f : UnitAddCircle → ℝ≥0∞<GOAL>∫⁻ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫⁻ (b : UnitAddCircle), f b
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : ℝ<VAR>f : UnitAddCircle → E<GOAL>∫ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫ (b : UnitAddCircle), f b
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : ℝ<VAR>f : UnitAddCircle → E<GOAL>∫ (a : ℝ) in t..t + 1, f ↑a = ∫ (b : UnitAddCircle), f b
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Function.Periodic f T<VAR>hT : 0 < T<VAR>t s : ℝ<GOAL>∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Function.Periodic f T<VAR>t s : ℝ<GOAL>∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Function.Periodic f T<VAR>t s : ℝ<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂<GOAL>∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in t..t + T, f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>T : ℝ<VAR>hf : Function.Periodic f T<VAR>n : ℤ<VAR>t : ℝ<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂<GOAL>∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x
<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Function.Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<GOAL>sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Set.Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤ ∫ (x : ℝ) in 0 ..t, g x
<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Function.Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂<VAR>hT : 0 < T<VAR>t : ℝ<GOAL>∫ (x : ℝ) in 0 ..t, g x ≤ sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Set.Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x
<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Function.Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atTop Filter.atTop
<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Function.Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂<VAR>h₀ : 0 < ∫ (x : ℝ) in 0 ..T, g x<VAR>hT : 0 < T<GOAL>Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atBot Filter.atBot
<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Function.Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂<VAR>h₀ : ∀ (x : ℝ), 0 < g x<VAR>hT : 0 < T<GOAL>Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atTop Filter.atTop
<VAR>T : ℝ<VAR>g : ℝ → ℝ<VAR>hg : Function.Periodic g T<VAR>h_int : ∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂<VAR>h₀ : ∀ (x : ℝ), 0 < g x<VAR>hT : 0 < T<GOAL>Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atBot Filter.atBot
<GOAL>MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
<VAR>p q : ℝ<VAR>hp : 0 < p<VAR>hq : -1 < q<GOAL>∫ (x : ℝ) in Set.Ioi 0, x ^ q * rexp (-x ^ p) = 1 / p * Real.Gamma ((q + 1) / p)
<VAR>p q b : ℝ<VAR>hp : 0 < p<VAR>hq : -1 < q<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Set.Ioi 0, x ^ q * rexp (-b * x ^ p) = b ^ (-(q + 1) / p) * (1 / p) * Real.Gamma ((q + 1) / p)
<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>∫ (x : ℝ) in Set.Ioi 0, rexp (-x ^ p) = Real.Gamma (1 / p + 1)
<VAR>p b : ℝ<VAR>hp : 0 < p<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Set.Ioi 0, rexp (-b * x ^ p) = b ^ (-1 / p) * Real.Gamma (1 / p + 1)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>I J : Finset ι<VAR>hP : MeasureTheory.IsProjectiveMeasureFamily P<VAR>hJI : J ⊆ I<GOAL>(P I) Set.univ = (P J) Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>hP : MeasureTheory.IsProjectiveMeasureFamily P<VAR>I J : Finset ι<GOAL>(P I) Set.univ = (P J) Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>I J : Finset ι<VAR>hP : MeasureTheory.IsProjectiveMeasureFamily P<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>hT : MeasurableSet T<VAR>h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T<VAR>hJI : J ⊆ I<GOAL>(P I) S = (P J) T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>I J : Finset ι<VAR>hP : MeasureTheory.IsProjectiveMeasureFamily P<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>T : Set ((i : { x // x ∈ J }) → α ↑i)<VAR>hS : MeasurableSet S<VAR>hT : MeasurableSet T<VAR>h_eq : MeasureTheory.cylinder I S = MeasureTheory.cylinder J T<GOAL>(P I) S = (P J) T
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ : MeasureTheory.Measure ((i : ι) → α i)<VAR>h : MeasureTheory.IsProjectiveLimit μ P<VAR>I : Finset ι<VAR>s : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>hs : MeasurableSet s<GOAL>μ (MeasureTheory.cylinder I s) = (P I) s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ : MeasureTheory.Measure ((i : ι) → α i)<VAR>hμ : MeasureTheory.IsProjectiveLimit μ P<VAR>I : Finset ι<GOAL>μ Set.univ = (P I) Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ : MeasureTheory.Measure ((i : ι) → α i)<VAR>∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)<VAR>hμ : MeasureTheory.IsProjectiveLimit μ P<GOAL>MeasureTheory.IsFiniteMeasure μ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ : MeasureTheory.Measure ((i : ι) → α i)<VAR>∀ (i : Finset ι), MeasureTheory.IsProbabilityMeasure (P i)<VAR>hμ : MeasureTheory.IsProjectiveLimit μ P<GOAL>MeasureTheory.IsProbabilityMeasure μ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : MeasureTheory.Measure ((i : ι) → α i)<VAR>hμ : MeasureTheory.IsProjectiveLimit μ P<VAR>hν : MeasureTheory.IsProjectiveLimit ν P<GOAL>μ Set.univ = ν Set.univ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → MeasureTheory.Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : MeasureTheory.Measure ((i : ι) → α i)<VAR>∀ (i : Finset ι), MeasureTheory.IsFiniteMeasure (P i)<VAR>hμ : MeasureTheory.IsProjectiveLimit μ P<VAR>hν : MeasureTheory.IsProjectiveLimit ν P<GOAL>μ = ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>TopologicalSpace β<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<GOAL>StronglyMeasurableAtFilter f ⊥ μ