ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E'<VAR>h_ae_eq_f : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯) =ᶠ[ae μ] fun a => ⟪c, ↑↑f a⟫_𝕜<GOAL>∫ (a : α) in s, ⟪c, ↑↑↑((condexpL2 E' 𝕜 hm) f) a⟫_𝕜 ∂μ - ∫ (a : α) in s, ⟪c, ↑↑f a⟫_𝕜 ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' 2 μ)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E'<VAR>h_ae_eq_f : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯) =ᶠ[ae μ] fun a => ⟪c, ↑↑f a⟫_𝕜<GOAL>∫ (x : α) in s, ↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) x ∂μ = ∫ (x : α) in s, ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯) x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y z : (i : ι) → β i<GOAL>hammingDist x y ≤ hammingDist z x + hammingDist z y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y z : (i : ι) → β i<GOAL>hammingDist x y ≤ hammingDist x z + hammingDist z y
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : NormedRing 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : MulActionWithZero 𝕜 E<VAR>inst✝³ : BoundedSMul 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : MulActionWithZero 𝕜 F<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : Memℒp f p μ<VAR>hφ : Memℒp φ ⊤ μ<GOAL>Memℒp (φ • f) p μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : NormedRing 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : MulActionWithZero 𝕜 E<VAR>inst✝³ : BoundedSMul 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : MulActionWithZero 𝕜 F<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f✝ : α → E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : Memℒp f p μ<VAR>hφ : Memℒp φ ⊤ μ<GOAL>1 / p = 1 / ⊤ + 1 / p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<GOAL>𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
<GOAL>∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b
<VAR>this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize<GOAL>∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<GOAL>Tendsto (fun n => ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x<GOAL>Tendsto (fun n => ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<GOAL>Tendsto (fun n => ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<GOAL>Tendsto (fun n => ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<GOAL>Tendsto (fun n => ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<GOAL>Tendsto (fun n => ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<GOAL>Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<GOAL>Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<VAR>h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)<GOAL>Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<GOAL>∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<VAR>h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)<GOAL>Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<VAR>h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)<GOAL>∀ (n : ℕ), AEMeasurable (fun a => ENNReal.ofReal (f' n a)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<VAR>h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)<GOAL>∀ᵐ (x : α) ∂μ, Monotone fun n => ENNReal.ofReal (f' n x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F✝ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace ℝ F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>μ : Measure α<VAR>f : ℕ → α → ℝ<VAR>F : α → ℝ<VAR>hf : ∀ (n : ℕ), Integrable (f n) μ<VAR>hF : Integrable F μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))<VAR>f' : ℕ → α → ℝ := fun n x => f n x - f 0 x<VAR>hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a<VAR>hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ<VAR>hF_ge : 0 ≤ᶠ[ae μ] fun x => (F - f 0) x<VAR>h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : CommSemiring A'<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R B<VAR>p q : R[X]<VAR>x : A<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Algebra S A'<VAR>inst✝ : Algebra S B<VAR>g : R →ₐ[S] A'<VAR>y : A'<VAR>s : S<GOAL>(aevalTower (AlgHom.id S S) s) X = (aeval s) X
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul αᵐᵒᵖ α<VAR>s t : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 1<GOAL>s * {a} ∈ 𝓝 a
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u<VAR>inst✝ : Field L<VAR>f : K →+* L<VAR>a : L<VAR>x : RatFunc K<VAR>h : Polynomial.eval₂ f a x.denom = 0<GOAL>eval f a x = 0
<VAR>P : AffineTargetMorphismProperty<VAR>inst✝³ : P.toProperty.RespectsIso<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝² : IsIso g<VAR>inst✝¹ : IsAffine Z<VAR>inst✝ : IsAffine Y<GOAL>P (f ≫ g) ↔ P f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜' E<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜' E<VAR>c : 𝕜<VAR>f : ↥(Lp E p μ)<GOAL>c • ↑f ∈ Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜' E<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜' E<VAR>c : 𝕜<VAR>f : ↥(Lp E p μ)<GOAL>eLpNorm (c • ↑↑f) p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜' E<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜' E<VAR>c : 𝕜<VAR>f : ↥(Lp E p μ)<GOAL>‖c‖₊ • eLpNorm (↑↑f) p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>𝕜' : Type u_6<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜' E<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜' E<VAR>c : 𝕜<VAR>f : ↥(Lp E p μ)<GOAL>↑‖c‖₊ < ⊤ ∧ eLpNorm (↑↑f) p μ < ⊤ ∨ ↑‖c‖₊ = 0 ∨ eLpNorm (↑↑f) p μ = 0
<VAR>m n : ℕ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>↑(m - n) = ↑m - ↑n
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>↑(m - n) = ↑m - ↑n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Inducing f<VAR>s : Set X<GOAL>IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f g : A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ zeroLocus 𝒜 {f * g} ↔ x ∈ zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS✝ : S ≤ A⁰<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>hS : S ≤ A⁰<VAR>x : B<GOAL>∃ a s, ∃ (hs : s ∈ S), (mapToFractionRing K S B hS).toRingHom x = IsLocalization.mk' K a ⟨s, ⋯⟩
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS✝ : S ≤ A⁰<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>hS : S ≤ A⁰<VAR>a : A<VAR>s : ↥S<GOAL>∃ a_1 s_1, ∃ (hs : s_1 ∈ S), (mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a s) = IsLocalization.mk' K a_1 ⟨s_1, ⋯⟩
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : CommRing A<VAR>S : Submonoid A<VAR>hS✝ : S ≤ A⁰<VAR>inst✝⁵ : CommRing K<VAR>inst✝⁴ : Algebra A K<VAR>inst✝³ : IsFractionRing A K<VAR>B : Type u_3<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsLocalization S B<VAR>hS : S ≤ A⁰<VAR>a : A<VAR>s : ↥S<GOAL>(mapToFractionRing K S B hS).toRingHom (IsLocalization.mk' B a s) = IsLocalization.mk' K a ⟨↑s, ⋯⟩