ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<GOAL>tsupport ↑f = closedBall c f.rOut
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0<VAR>H' : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = ⊤)<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0<VAR>H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0<VAR>H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤<VAR>this : ↑(∑ i ∈ s, (fun i => (f i).toNNReal) i * (fun i => (g i).toNNReal) i) ≤ ↑((∑ i ∈ s, (fun i => (f i).toNNReal) i ^ p) ^ (1 / p) * (∑ i ∈ s, (fun i => (g i).toNNReal) i ^ q) ^ (1 / q))<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>H : (∑ i ∈ s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≠ 0<VAR>H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤<VAR>this : ∑ x ∈ s, ↑(f x).toNNReal * ↑(g x).toNNReal ≤ (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ p⁻¹ * (∑ x ∈ s, ↑(g x).toNNReal ^ q) ^ q⁻¹<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>0 < G.chromaticNumber
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>0 < sInf {n' | G.Colorable n'}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>∀ b ∈ {n | G.Colorable n}, Nat.succ 0 ≤ b
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<VAR>m : ℕ<VAR>hm : m ∈ {n | G.Colorable n}<GOAL>Nat.succ 0 ≤ m
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<VAR>m : ℕ<VAR>hm : m ∈ {n | G.Colorable n}<VAR>h' : ¬Nat.succ 0 ≤ m<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<VAR>m : ℕ<VAR>hm : m ∈ {n | G.Colorable n}<VAR>h' : m < Nat.succ 0<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<VAR>m : ℕ<VAR>hm : m ∈ {n | G.Colorable n}<VAR>h' : m < Nat.succ 0<VAR>i : ℕ<VAR>hi : i < m<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>inst✝ : Nonempty V<VAR>n : ℕ<VAR>hc : G.Colorable n<VAR>m : ℕ<VAR>hm : m ∈ {n | G.Colorable n}<VAR>h' : m < Nat.succ 0<VAR>i : ℕ<VAR>hi : i < m<VAR>h₁ : i < 0<GOAL>False
<VAR>X : Type u_1<VAR>inst✝⁸ : TopologicalSpace X<VAR>inst✝⁷ : Zero X<VAR>A : Type u_2<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Module ℝ A<VAR>inst✝² : IsScalarTower ℝ A A<VAR>inst✝¹ : SMulCommClass ℝ A A<VAR>inst✝ : TopologicalRing A<VAR>φ ψ : C(X, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A<VAR>h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal<VAR>f : C(X, ℝ≥0)₀<GOAL>φ f = ψ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<GOAL>log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<GOAL>log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<GOAL>0 < 2 / (1 - 2 / rexp 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<GOAL>log 8 * (69 / 50) ≤ √(log ↑N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>log 8 * (69 / 50) ≤ √(log ↑N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>↑3 * log 2 * (69 / 50) ≤ √(log ↑N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>(↑3 * log 2 * (69 / 50)) ^ 2 ≤ ↑12 * log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>(↑3 * (69 / 50)) ^ 2 * log 2 * log 2 ≤ ↑12 * log 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>(↑3 * (69 / 50)) ^ 2 * log 2 ≤ ↑12
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>log 2 ≤ ↑12 / (↑3 * (69 / 50)) ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 4096 ≤ N<VAR>this : ↑12 * log 2 ≤ log ↑N<VAR>l8 : log 8 = ↑3 * log 2<GOAL>0 < (↑3 * (69 / 50)) ^ 2
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C<VAR>θ : ℝ<VAR>x✝ : θ ∈ Ι 0 (2 * π)<GOAL>‖deriv (circleMap c R) θ • f (circleMap c R θ)‖ = |R| * ‖f (circleMap c R θ)‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C<GOAL>|R| * C * |2 * π - 0| = 2 * π * |R| * C
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hf : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C<GOAL>|R| * C * (2 * π) = 2 * π * |R| * C
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>ConvolutionExistsAt f g x₀ L μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>HasCompactSupport fun t => (L (f t)) (g (x₀ - t))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>(support fun t => (L (f t)) (g (x₀ - t))) ⊆ support (g ∘ ⇑(Homeomorph.subLeft x₀))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 E'<VAR>inst✝⁶ : NormedSpace 𝕜 E''<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁴ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝³ : AddGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : BorelSpace G<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : Continuous g<VAR>x₀ t : G<VAR>ht : g (x₀ - t) = 0<GOAL>(fun t => (L (f t)) (g (x₀ - t))) t = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Subsingleton M<GOAL>finrank R M = 0
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddAbove (range f)<GOAL>⋃ i, Iic (f i) = univ
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddAbove (range f)<GOAL>⋃ i, Iio (f i) ⊆ ⋃ i, Iic (f i)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>hf : ¬BddAbove (range f)<VAR>i✝ : ι<GOAL>Iio (f i✝) ⊆ Iic (f i✝)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<VAR>e0 : e = 0<GOAL>a = 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<GOAL>μ s = 0 ∨ μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s = 0<GOAL>μ s = 0 ∨ μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<GOAL>μ s = 0 ∨ μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<GOAL>μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>hd : ∀ {ι' : Type ?u.7040} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) → Tendsto (fun j => μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)<GOAL>μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>hd : ∀ {ι' : Type ?u.7040} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) → Tendsto (fun j => μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<GOAL>μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<GOAL>μ s = ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<GOAL>∀ᶠ (j : ι) in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<VAR>this : addOrderOf (u j) = n j<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<VAR>this : addOrderOf (u j) = n j<VAR>huj : IsOfFinAddOrder (u j)<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<VAR>this : addOrderOf (u j) = n j<VAR>huj : IsOfFinAddOrder (u j)<VAR>huj' : 1 ≤ ↑(n j)<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<VAR>this : addOrderOf (u j) = n j<VAR>huj : IsOfFinAddOrder (u j)<VAR>huj' : 1 ≤ ↑(n j)<VAR>hI₀ : μ (I j) ≠ 0<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<VAR>this : addOrderOf (u j) = n j<VAR>huj : IsOfFinAddOrder (u j)<VAR>huj' : 1 ≤ ↑(n j)<VAR>hI₀ : μ (I j) ≠ 0<VAR>hI₁ : μ (I j) ≠ ⊤<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>s : Set (AddCircle T)<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>u : ι → AddCircle T<VAR>μ : Measure (AddCircle T) := volume<VAR>hs : NullMeasurableSet s μ<VAR>hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s<VAR>n : ι → ℕ := addOrderOf ∘ u<VAR>hu₂ : Tendsto n l atTop<VAR>hT₀ : 0 < T<VAR>hT₁ : ENNReal.ofReal T ≠ 0<VAR>h : μ s ≠ 0<VAR>d : AddCircle T<VAR>I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))<VAR>hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)<VAR>j : ι<VAR>hj : 0 < n j<VAR>this : addOrderOf (u j) = n j<VAR>huj : IsOfFinAddOrder (u j)<VAR>huj' : 1 ≤ ↑(n j)<VAR>hI₀ : μ (I j) ≠ 0<VAR>hI₁ : μ (I j) ≠ ⊤<VAR>hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T<GOAL>μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDomain A<VAR>I : Ideal A<VAR>hI : I ≠ ⊥<GOAL>1 ∈ (↑I)⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDomain A<VAR>I : Ideal A<VAR>hI : I ≠ ⊥<GOAL>∀ y ∈ ↑I, 1 * y ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDomain A<VAR>I : Ideal A<VAR>hI : I ≠ ⊥<VAR>y : K<VAR>hy : y ∈ ↑I<GOAL>1 * y ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDomain A<VAR>I : Ideal A<VAR>hI : I ≠ ⊥<VAR>y : K<VAR>hy : y ∈ ↑I<GOAL>y ∈ 1
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>x : α<GOAL>(𝓝 x).HasBasis p fun i => ball x (s i)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>x : α<GOAL>(comap (Prod.mk x) (𝓤 α)).HasBasis p fun i => ball x (s i)
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>n : ℕ<GOAL>↑(x ^ ↑n) = ↑(x ^ n)
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>H : CompactSpace ↑↑X.toPresheafedSpace<GOAL>X.OpenCover
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>H : CompactSpace ↑↑X.toPresheafedSpace<VAR>this : ∃ t, ⋃ x ∈ t, (fun x => Set.range ⇑(𝒰.map (𝒰.f x)).val.base) x = ⊤<GOAL>X.OpenCover
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>H : CompactSpace ↑↑X.toPresheafedSpace<VAR>this : ∃ t, ⋃ x ∈ t, (fun x => Set.range ⇑(𝒰.map (𝒰.f x)).val.base) x = ⊤<VAR>t : Finset ↑↑X.toPresheafedSpace := this.choose<GOAL>X.OpenCover
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>H : CompactSpace ↑↑X.toPresheafedSpace<VAR>this : ∃ t, ⋃ x ∈ t, (fun x => Set.range ⇑(𝒰.map (𝒰.f x)).val.base) x = ⊤<VAR>t : Finset ↑↑X.toPresheafedSpace := this.choose<VAR>h : ∀ (x : ↑↑X.toPresheafedSpace), ∃ y, x ∈ Set.range ⇑(𝒰.map (𝒰.f ↑y)).val.base<GOAL>X.OpenCover
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>mgf 0 μ t = (μ Set.univ).toReal