ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>chaar K₀ K₁ + chaar K₀ K₂ - chaar K₀ (K₁ ⊔ K₂) = 0
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<VAR>V : Set G := V₁ ∩ V₂<GOAL>chaar K₀ ∈ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<VAR>V : Set G := V₁ ∩ V₂<GOAL>clPrehaar ↑K₀ { carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ } ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<VAR>V : Set G := V₁ ∩ V₂<GOAL>closure (prehaar ↑K₀ '' {U | U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens ∧ IsOpen U ∧ 1 ∈ U}) ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<VAR>V : Set G := V₁ ∩ V₂<GOAL>prehaar ↑K₀ '' {U | U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens ∧ IsOpen U ∧ 1 ∈ U} ⊆ eval ⁻¹' {0}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<VAR>V : Set G := V₁ ∩ V₂<GOAL>IsClosed (eval ⁻¹' {0})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>hf : Measurable f<VAR>κ : Kernel α β<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((deterministic f hf ∘ₖ κ) a) s = ((κ.map f hf) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>γ : Type u_3<VAR>inst✝¹ : AddCommMonoid β<VAR>inst✝ : ContinuousAdd β<VAR>f : γ → C(α, β)<VAR>g : C(α, β)<VAR>hf : HasSum f g<VAR>x : α<VAR>ev : C(α, β) →+ β := (Pi.evalAddMonoidHom (fun a => β) x).comp coeFnAddMonoidHom<GOAL>HasSum (fun i => (f i) x) (g x)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<VAR>this : ∀ (i : ℕ), ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<GOAL>∀ᵐ (ω : Ω), (fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<VAR>this : ∀ (i : ℕ), ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<GOAL>(fun n => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop] fun n => ↑⌊c ^ n⌋₊
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<VAR>this : ∀ (i : ℕ), ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a‖ ≤ ε * ‖↑⌊c ^ x⌋₊‖
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<VAR>this : ∀ (i : ℕ), ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>i : ℕ<VAR>hi : v i < ε<GOAL>∀ᶠ (x : ℕ) in atTop, ‖∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a‖ ≤ ε * ‖↑⌊c ^ x⌋₊‖
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<VAR>this : ∀ (i : ℕ), ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>i : ℕ<VAR>hi : v i < ε<VAR>n : ℕ<VAR>hn : |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<GOAL>‖∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a‖ ≤ ε * ‖↑⌊c ^ n⌋₊‖
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>c : ℝ<VAR>c_one : 1 < c<VAR>v : ℕ → ℝ<VAR>v_pos : ∀ (n : ℕ), 0 < v n<VAR>v_lim : Tendsto v atTop (𝓝 0)<VAR>this : ∀ (i : ℕ), ∀ᵐ (ω : Ω), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ω : Ω<VAR>hω : ∀ (i : ℕ), ∀ᶠ (n : ℕ) in atTop, |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>i : ℕ<VAR>hi : v i < ε<VAR>n : ℕ<VAR>hn : |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| < v i * ↑⌊c ^ n⌋₊<GOAL>|∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| ≤ ε * ↑⌊c ^ n⌋₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>y : α<VAR>h_disjoint : s.PairwiseDisjoint f<VAR>hy : y ∈ ⋃ i ∈ s, f i<GOAL>∃! i, i ∈ s ∧ y ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>y : α<VAR>h_disjoint : s.PairwiseDisjoint f<VAR>hy : y ∈ ⋃ i ∈ s, f i<GOAL>∃ x ∈ s, y ∈ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>y : α<VAR>h_disjoint : s.PairwiseDisjoint f<VAR>hy : y ∈ ⋃ i ∈ s, f i<GOAL>∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m * m = n * n ↔ m = n
<VAR>n m : ℕ+<VAR>u : PrimeMultiset := n.factorMultiset<VAR>v : PrimeMultiset := m.factorMultiset<GOAL>(n * m).factorMultiset = n.factorMultiset + m.factorMultiset
<VAR>n m : ℕ+<VAR>u : PrimeMultiset := n.factorMultiset<VAR>v : PrimeMultiset := m.factorMultiset<VAR>this : n = u.prod<GOAL>(n * m).factorMultiset = n.factorMultiset + m.factorMultiset
<VAR>n m : ℕ+<VAR>u : PrimeMultiset := n.factorMultiset<VAR>v : PrimeMultiset := m.factorMultiset<VAR>this : n = u.prod<GOAL>(u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset
<VAR>n m : ℕ+<VAR>u : PrimeMultiset := n.factorMultiset<VAR>v : PrimeMultiset := m.factorMultiset<VAR>this✝ : n = u.prod<VAR>this : m = v.prod<GOAL>(u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset
<VAR>n m : ℕ+<VAR>u : PrimeMultiset := n.factorMultiset<VAR>v : PrimeMultiset := m.factorMultiset<VAR>this✝ : n = u.prod<VAR>this : m = v.prod<GOAL>(u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
<VAR>n m : ℕ+<VAR>u : PrimeMultiset := n.factorMultiset<VAR>v : PrimeMultiset := m.factorMultiset<VAR>this✝ : n = u.prod<VAR>this : m = v.prod<GOAL>(u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>Hf : ∀ a ∈ s, f a ∈ t<VAR>n : ℕ<VAR>hn : ∀ a ∈ t, (filter (fun x => f x = a) s).card ≤ n<GOAL>∑ _a ∈ t, n = n * t.card
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹³ : CommRing R₁<VAR>inst✝¹² : AddCommGroup M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : CommRing R₃<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>inst✝¹ : Fintype n<VAR>b : Basis n R₃ M₃<VAR>J J₃ A A' : Matrix n n R₃<VAR>inst✝ : DecidableEq n<GOAL>A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A
<VAR>a b r : ℤ<VAR>hr : 0 < r<GOAL>↑(filter (fun x => r ∣ x) (Ico a b)).card = max (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>(TensorProduct.mk R ↑M ↑(of R R)).compr₂ (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = (TensorProduct.mk R ↑M ↑(of R R)).compr₂ ((rightUnitor M).hom ≫ f)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>∀ (x : ↑M), ((TensorProduct.mk R ↑M ↑(of R R)).compr₂ (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x = ((TensorProduct.mk R ↑M ↑(of R R)).compr₂ ((rightUnitor M).hom ≫ f)) x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>((TensorProduct.mk R ↑M ↑(of R R)).compr₂ (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x = ((TensorProduct.mk R ↑M ↑(of R R)).compr₂ ((rightUnitor M).hom ≫ f)) x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(((TensorProduct.mk R ↑M ↑(of R R)).compr₂ (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x) 1 = (((TensorProduct.mk R ↑M ↑(of R R)).compr₂ ((rightUnitor M).hom ≫ f)) x) 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(rightUnitor N).hom ((tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] 1)) = f ((rightUnitor M).hom (x ⊗ₜ[R] 1))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(𝟙 (of R R)) (x, 1).2 • f (x, 1).1 = f (1 • x)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↑M<GOAL>(𝟙 (of R R)) (x, 1).2 • f (x, 1).1 = 1 • f x
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedSinZeta (-a) s = -completedSinZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>(∫ (t : ℝ) in Ioi 0, -(↑t ^ ((s + 1) / 2 - 1) • ↑(sinKernel a t))) / 2 = -((∫ (t : ℝ) in Ioi 0, ↑t ^ ((s + 1) / 2 - 1) • ↑(sinKernel a t)) / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : Summable fun n => f n x₀<VAR>hx : x ∈ s<GOAL>HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>inst✝⁴ : CommRing 𝒪<VAR>inst✝³ : IsDomain 𝒪<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra 𝒪 K<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<VAR>a b : 𝒪<GOAL>∃ c, a * c = b ∨ b * c = a
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>inst✝⁴ : CommRing 𝒪<VAR>inst✝³ : IsDomain 𝒪<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra 𝒪 K<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<VAR>a b : 𝒪<VAR>h : v ((algebraMap 𝒪 K) a) ≤ v ((algebraMap 𝒪 K) b)<GOAL>∃ c, a * c = b ∨ b * c = a
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>inst✝⁴ : CommRing 𝒪<VAR>inst✝³ : IsDomain 𝒪<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra 𝒪 K<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<VAR>a b : 𝒪<VAR>h : v ((algebraMap 𝒪 K) b) ≤ v ((algebraMap 𝒪 K) a)<GOAL>∃ c, a * c = b ∨ b * c = a
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>inst✝¹ : HasWeakSheafify J A<VAR>inst✝ : J.WEqualsLocallyBijective A<VAR>P Q : Cᵒᵖ ⥤ A<VAR>φ : P ⟶ Q<GOAL>Sheaf.IsLocallyInjective ((presheafToSheaf J A).map φ) ↔ IsLocallyInjective J φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g✝ : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hg' : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ≥0∞<VAR>hε : ε > 0<VAR>hfinε : ε ≠ ⊤<VAR>hμ : ¬μ = 0<VAR>hε' : 0 < ε / 3<VAR>Eg : Set α<VAR>hmEg : MeasurableSet Eg<VAR>hμEg : μ Eg < ⊤<VAR>hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3<VAR>Ef : Set α<VAR>hmEf : MeasurableSet Ef<VAR>hμEf : μ Ef < ⊤<VAR>hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3<VAR>hmE : MeasurableSet (Ef ∪ Eg)<GOAL>∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε