ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Integrable f μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ = ∫ (x : Ω) in s, f x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Integrable f μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>(μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Memℒp f 1 μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>(μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Memℒp f 1 μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>AEStronglyMeasurable' m₁ f μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Memℒp f 1 μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>∀ (c : E) ⦃s_1 : Set Ω⦄, MeasurableSet s_1 → μ s_1 < ⊤ → (μ s).toReal • ∫ (x : Ω), s_1.indicator (fun x => c) x ∂μ = ∫ (x : Ω) in s, s_1.indicator (fun x => c) x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Memℒp f 1 μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>∀ ⦃f g : Ω → E⦄, Disjoint (Function.support f) (Function.support g) → Memℒp f 1 μ → Memℒp g 1 μ → StronglyMeasurable f → StronglyMeasurable g → (μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → (μ s).toReal • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ → (μ s).toReal • ∫ (x : Ω), (f + g) x ∂μ = ∫ (x : Ω) in s, (f + g) x ∂μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Memℒp f 1 μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>IsClosed {f | (μ s).toReal • ∫ (x : Ω), ↑↑↑f x ∂μ = ∫ (x : Ω) in s, ↑↑↑f x ∂μ}
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Memℒp f 1 μ<VAR>s : Set Ω<VAR>hms : MeasurableSet s<VAR>hs : μ s < ⊤<GOAL>∀ ⦃f g : Ω → E⦄, f =ᶠ[ae μ] g → Memℒp f 1 μ → (μ s).toReal • ∫ (x : Ω), f x ∂μ = ∫ (x : Ω) in s, f x ∂μ → (μ s).toReal • ∫ (x : Ω), g x ∂μ = ∫ (x : Ω) in s, g x ∂μ
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>this : l.NeBot<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>this : l.NeBot<VAR>hr : r ≤ 0<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : UniformCauchySeqOn f' l (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>this : l.NeBot<VAR>hr : 0 < r<GOAL>UniformCauchySeqOn f l (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : TendstoUniformlyOn (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>this : l.NeBot<VAR>hr : 0 < r<GOAL>TendstoUniformlyOn (fun n z => f n.1 z - f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>r : ℝ<VAR>hf' : TendstoUniformlyOn (fun n z => f' n.1 z - f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)<VAR>hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y<VAR>hfg : Cauchy (map (fun n => f n x) l)<VAR>this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>this : l.NeBot<VAR>hr : 0 < r<GOAL>TendstoUniformlyOn (fun n z => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r) ∧ TendstoUniformlyOn (fun n x_1 => f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>t : Set Y<VAR>h : MapsTo f s t<VAR>hc : Continuous f<GOAL>MapsTo f (closure s) (closure t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>t : Set Y<VAR>h : MapsTo f s t<VAR>hc : Continuous f<GOAL>∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<GOAL>False
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<GOAL>ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<GOAL>((fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) ∘ ε) n ≤ 1 - ENNReal.ofReal (4⁻¹ ^ Fintype.card ι)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>ε n ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 < (2 * ε n) ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 < ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) → ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) < ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) → ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 ≤ ε n / 4
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 ≤ ε n
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>MeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁷ : Semifield R<VAR>inst✝²⁶ : StarRing R<VAR>inst✝²⁵ : MetricSpace R<VAR>inst✝²⁴ : TopologicalSemiring R<VAR>inst✝²³ : ContinuousStar R<VAR>inst✝²² : Field S<VAR>inst✝²¹ : StarRing S<VAR>inst✝²⁰ : MetricSpace S<VAR>inst✝¹⁹ : TopologicalRing S<VAR>inst✝¹⁸ : ContinuousStar S<VAR>inst✝¹⁷ : TopologicalSpace A<VAR>inst✝¹⁶ : NonUnitalRing A<VAR>inst✝¹⁵ : StarRing A<VAR>inst✝¹⁴ : Module S A<VAR>inst✝¹³ : IsScalarTower S A A<VAR>inst✝¹² : SMulCommClass S A A<VAR>inst✝¹¹ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : IsScalarTower R S A<VAR>inst✝⁷ : StarModule R S<VAR>inst✝⁶ : ContinuousSMul R S<VAR>inst✝⁵ : CompleteSpace R<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝¹ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : QuasispectrumRestricts a ⇑f<VAR>inst✝ : CompactSpace ↑(σₙ S a)<GOAL>cfcₙHom hpa = nonUnitalStarAlgHom (cfcₙHom hqa) h
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁷ : Semifield R<VAR>inst✝²⁶ : StarRing R<VAR>inst✝²⁵ : MetricSpace R<VAR>inst✝²⁴ : TopologicalSemiring R<VAR>inst✝²³ : ContinuousStar R<VAR>inst✝²² : Field S<VAR>inst✝²¹ : StarRing S<VAR>inst✝²⁰ : MetricSpace S<VAR>inst✝¹⁹ : TopologicalRing S<VAR>inst✝¹⁸ : ContinuousStar S<VAR>inst✝¹⁷ : TopologicalSpace A<VAR>inst✝¹⁶ : NonUnitalRing A<VAR>inst✝¹⁵ : StarRing A<VAR>inst✝¹⁴ : Module S A<VAR>inst✝¹³ : IsScalarTower S A A<VAR>inst✝¹² : SMulCommClass S A A<VAR>inst✝¹¹ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : IsScalarTower R S A<VAR>inst✝⁷ : StarModule R S<VAR>inst✝⁶ : ContinuousSMul R S<VAR>inst✝⁵ : CompleteSpace R<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝¹ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : QuasispectrumRestricts a ⇑f<VAR>inst✝ : CompactSpace ↑(σₙ S a)<GOAL>Continuous ⇑(nonUnitalStarAlgHom (cfcₙHom hqa) h)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁷ : Semifield R<VAR>inst✝²⁶ : StarRing R<VAR>inst✝²⁵ : MetricSpace R<VAR>inst✝²⁴ : TopologicalSemiring R<VAR>inst✝²³ : ContinuousStar R<VAR>inst✝²² : Field S<VAR>inst✝²¹ : StarRing S<VAR>inst✝²⁰ : MetricSpace S<VAR>inst✝¹⁹ : TopologicalRing S<VAR>inst✝¹⁸ : ContinuousStar S<VAR>inst✝¹⁷ : TopologicalSpace A<VAR>inst✝¹⁶ : NonUnitalRing A<VAR>inst✝¹⁵ : StarRing A<VAR>inst✝¹⁴ : Module S A<VAR>inst✝¹³ : IsScalarTower S A A<VAR>inst✝¹² : SMulCommClass S A A<VAR>inst✝¹¹ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : IsScalarTower R S A<VAR>inst✝⁷ : StarModule R S<VAR>inst✝⁶ : ContinuousSMul R S<VAR>inst✝⁵ : CompleteSpace R<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝¹ : UniqueNonUnitalContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : QuasispectrumRestricts a ⇑f<VAR>inst✝ : CompactSpace ↑(σₙ S a)<GOAL>(nonUnitalStarAlgHom (cfcₙHom hqa) h) { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } = a
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>h : M.Basis' I X<GOAL>M.Basis I (M.closure X)
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>h : M.Basis' I X<GOAL>M.Basis I (M.closure I)
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h✝ : ContfracLegendre.Ass ξ u v<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<GOAL>∃ n, q = ξ.convergent n
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h✝ : ContfracLegendre.Ass ξ u v<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<GOAL>IsCoprime q.num ↑q.den
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h✝ : ContfracLegendre.Ass ξ u v<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<VAR>hd : ↑q.den = 1<GOAL>-(1 / 2) < ξ - ↑q.num
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h✝ : ContfracLegendre.Ass ξ u v<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<GOAL>|ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hf : ((expand F (p ^ n)) f).Separable<GOAL>IsUnit f ∨ n = 0
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hf : ((expand F (p ^ n)) f).Separable<GOAL>¬n = 0 → IsUnit f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hf : ((expand F (p ^ n)) f).Separable<VAR>hn : n ≠ 0<GOAL>IsUnit f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hf : ((expand F (p ^ n)) f).Separable<VAR>hn : n ≠ 0<VAR>hf2 : derivative ((expand F (p ^ n)) f) = 0<GOAL>IsUnit f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hf : ∃ r, IsUnit r ∧ C r = (expand F (p ^ n)) f<VAR>hn : n ≠ 0<VAR>hf2 : derivative ((expand F (p ^ n)) f) = 0<GOAL>IsUnit f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hn : n ≠ 0<VAR>hf2 : derivative ((expand F (p ^ n)) f) = 0<VAR>r : F<VAR>hr : IsUnit r<VAR>hrf : C r = (expand F (p ^ n)) f<GOAL>IsUnit f
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>HF : CharP F p<VAR>f : F[X]<VAR>n : ℕ<VAR>hp : 0 < p<VAR>hn : n ≠ 0<VAR>hf2 : derivative ((expand F (p ^ n)) f) = 0<VAR>r : F<VAR>hr : IsUnit r<VAR>hrf : f = C r<GOAL>IsUnit f
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>addValuationDef 1 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>s \ t ∪ s ∩ t = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<GOAL>s ∩ t ∪ s \ t = s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arcsin (dist p₃ p₂ / dist p₁ p₃))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2<GOAL>(Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal) ↔ (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2<GOAL>(∀ (x : S), ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x = (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x) ↔ ∀ (x : S), ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2<GOAL>∀ (a : S), ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) a = (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) a ↔ ((TensorProduct.lmul' R).kerSquareLift.comp f) a = (AlgHom.id R S) a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2<VAR>x : S<GOAL>((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x = (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x