ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>RCLike K<VAR>x y : K<GOAL>(starRingEnd K) (x / y) = (starRingEnd K) x / (starRingEnd K) y
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : K<GOAL>∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : K<GOAL>∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
<VAR>K : Type u_1<VAR>RCLike K<VAR>r s : ℝ<GOAL>↑(r / s) = ↑r / ↑s
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<VAR>r : ℝ<GOAL>RCLike.re (z / ↑r) = RCLike.re z / r
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>n : ℤ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.I ≠ 0 → RCLike.I * RCLike.I = -1
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.I⁻¹ = -RCLike.I
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z / RCLike.I = -(z * RCLike.I)
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.normSq z⁻¹ = (RCLike.normSq z)⁻¹
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>RCLike.normSq (z / w) = RCLike.normSq z / RCLike.normSq w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>‖(starRingEnd K) z‖ = ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<GOAL>RCLike.re ↑n = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<GOAL>RCLike.im ↑n = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>RCLike.re (OfNat.ofNat n) = OfNat.ofNat n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>RCLike.im (OfNat.ofNat n) = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>z : K<GOAL>RCLike.re (OfNat.ofNat n * z) = OfNat.ofNat n * RCLike.re z
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>z : K<GOAL>RCLike.im (OfNat.ofNat n * z) = OfNat.ofNat n * RCLike.im z
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℤ<GOAL>↑↑n = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℤ<GOAL>RCLike.re ↑n = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℤ<GOAL>RCLike.im ↑n = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℚ<GOAL>↑↑n = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>q : ℚ<GOAL>RCLike.re ↑q = ↑q
<VAR>K : Type u_1<VAR>RCLike K<VAR>q : ℚ<GOAL>RCLike.im ↑q = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>r : ℝ<VAR>h : 0 ≤ r<GOAL>‖↑r‖ = r
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<GOAL>‖↑n‖ = ↑n
<VAR>K : Type u_1<VAR>RCLike K<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>‖OfNat.ofNat n‖ = OfNat.ofNat n
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>RCLike K<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>n : ℕ<VAR>x : E<GOAL>‖n • x‖ = n • ‖x‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>‖z‖ * ‖z‖ = RCLike.normSq z
<VAR>K : Type u_1<VAR>RCLike K<GOAL>‖2‖ = 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>|RCLike.re z| ≤ ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>|RCLike.im z| ≤ ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>‖RCLike.re z‖ ≤ ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>‖RCLike.im z‖ ≤ ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.re z ≤ ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>RCLike.im z ≤ ‖z‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>a : K<VAR>h : ‖a‖ ≤ RCLike.re a<GOAL>RCLike.im a = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>a : K<VAR>h : ‖a‖ ≤ RCLike.re a<GOAL>↑(RCLike.re a) = a
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>|RCLike.re z / ‖z‖| ≤ 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>|RCLike.im z / ‖z‖| ≤ 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>hI : RCLike.I ≠ 0<GOAL>‖RCLike.I‖ = 1
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : K<GOAL>RCLike.re (x * (starRingEnd K) x) = ‖x * (starRingEnd K) x‖
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : K<GOAL>‖x + (starRingEnd K) x‖ ^ 2 = RCLike.re (x + (starRingEnd K) x) ^ 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : K<GOAL>‖(starRingEnd K) x + x‖ ^ 2 = RCLike.re ((starRingEnd K) x + x) ^ 2
<VAR>K : Type u_1<VAR>RCLike K<VAR>f : CauSeq K norm<GOAL>IsCauSeq abs fun n => RCLike.re (↑f n)
<VAR>K : Type u_1<VAR>RCLike K<VAR>f : CauSeq K norm<GOAL>IsCauSeq abs fun n => RCLike.im (↑f n)
<VAR>K : Type u_1<VAR>RCLike K<VAR>f : ℕ → K<VAR>hf : IsCauSeq norm f<GOAL>IsCauSeq abs (norm ∘ f)
<VAR>K : Type u_1<VAR>RCLike K<VAR>z w : K<GOAL>z < w ↔ RCLike.re z < RCLike.re w ∧ RCLike.im z = RCLike.im w
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 ≤ z ↔ 0 ≤ RCLike.re z ∧ RCLike.im z = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 < z ↔ 0 < RCLike.re z ∧ RCLike.im z = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z ≤ 0 ↔ RCLike.re z ≤ 0 ∧ RCLike.im z = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z < 0 ↔ RCLike.re z < 0 ∧ RCLike.im z = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 ≤ z ↔ ∃ x ≥ 0, ↑x = z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 < z ↔ ∃ x > 0, ↑x = z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>z < 0 ↔ ∃ x < 0, ↑x = z
<VAR>K : Type u_1<VAR>RCLike K<VAR>x y : ℝ<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>K : Type u_1<VAR>RCLike K<VAR>x y : ℝ<GOAL>↑x < ↑y ↔ x < y
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>0 ≤ ↑x ↔ 0 ≤ x
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>↑x ≤ 0 ↔ x ≤ 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>0 < ↑x ↔ 0 < x
<VAR>K : Type u_1<VAR>RCLike K<VAR>x : ℝ<GOAL>↑x < 0 ↔ x < 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<VAR>hz : 0 < z<GOAL>0 < z⁻¹
<VAR>K : Type u_1<VAR>RCLike K<VAR>z : K<GOAL>0 < z⁻¹ ↔ 0 < z
<VAR>K : Type u_1<VAR>RCLike K<GOAL>StarOrderedRing K
<VAR>K : Type u_1<VAR>RCLike K<GOAL>OrderedSMul ℝ K
<VAR>K : Type u_1<VAR>RCLike K<VAR>A : Type u_3<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module K A<VAR>StarModule K A<VAR>IsScalarTower K A A<VAR>SMulCommClass K A A<GOAL>OrderedSMul K A
<VAR>x : ℝ<GOAL>RCLike.re x = x
<VAR>x : ℝ<GOAL>RCLike.im x = 0
<VAR>x : ℝ<GOAL>(starRingEnd ℝ) x = x
<VAR>x : ℝ<GOAL>RCLike.normSq x = x * x
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.reLm = ⇑RCLike.re
<VAR>K : Type u_1<VAR>RCLike K<GOAL>↑RCLike.reCLM = RCLike.reLm
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.reCLM = ⇑RCLike.re
<VAR>K : Type u_1<VAR>RCLike K<GOAL>Continuous ⇑RCLike.re
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.imLm = ⇑RCLike.im
<VAR>K : Type u_1<VAR>RCLike K<GOAL>↑RCLike.imCLM = RCLike.imLm
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.imCLM = ⇑RCLike.im
<VAR>K : Type u_1<VAR>RCLike K<GOAL>Continuous ⇑RCLike.im
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.conjAe = ⇑(starRingEnd K)
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.conjLIE = ⇑(starRingEnd K)
<VAR>K : Type u_1<VAR>RCLike K<GOAL>RCLike.conjCLE.toLinearEquiv = RCLike.conjAe.toLinearEquiv
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.conjCLE = ⇑(starRingEnd K)
<VAR>K : Type u_1<VAR>RCLike K<GOAL>Continuous ⇑(starRingEnd K)
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.ofRealAm = RCLike.ofReal
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.ofRealLI = RCLike.ofReal
<VAR>K : Type u_1<VAR>RCLike K<GOAL>↑RCLike.ofRealCLM = RCLike.ofRealAm.toLinearMap
<VAR>K : Type u_1<VAR>RCLike K<GOAL>⇑RCLike.ofRealCLM = RCLike.ofReal
<VAR>K : Type u_1<VAR>RCLike K<GOAL>Continuous RCLike.ofReal
<VAR>K : Type u_1<VAR>RCLike K<GOAL>Continuous ⇑RCLike.normSq
<VAR>K : Type u_1<VAR>RCLike K<VAR>h : RCLike.I = 0<VAR>z : K<GOAL>RCLike.im z = 0
<VAR>K : Type u_1<VAR>RCLike K<VAR>h : RCLike.I = 0<GOAL>∀ (a : ℝ), (RCLike.realRingEquiv h).symm a = ↑a
<VAR>K : Type u_1<VAR>RCLike K<VAR>h : RCLike.I = 0<VAR>a : K<GOAL>(RCLike.realRingEquiv h) a = RCLike.re a
<VAR>K : Type u_1<VAR>RCLike K<VAR>h : RCLike.I = 0<GOAL>∀ (a : K), (RCLike.realLinearIsometryEquiv h) a = (RCLike.realRingEquiv h).toFun a
<VAR>K : Type u_1<VAR>RCLike K<VAR>h : RCLike.I = 0<GOAL>∀ (a : ℝ), (RCLike.realLinearIsometryEquiv h).invFun a = (RCLike.realRingEquiv h).invFun a
<VAR>K : Type u_1<VAR>RCLike K<VAR>h : RCLike.I = 0<GOAL>∀ (a : ℝ), (RCLike.realLinearIsometryEquiv h).symm a = (RCLike.realRingEquiv h).invFun a
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a : ℕ → E<GOAL>HasSum (fun n => 0 ^ n • a n) (a 0)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : E<VAR>n : ℕ<VAR>z : 𝕜<VAR>a : ℕ → E<VAR>hs : HasSum (fun m => z ^ m • a m) s<VAR>ha : ∀ k < n, a k = 0<GOAL>∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<GOAL>HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>n : ℕ<VAR>hp : HasFPowerSeriesAt f p z₀<GOAL>HasFPowerSeriesAt ((Function.swap dslope z₀)^[n] f) (FormalMultilinearSeries.fslope^[n] p) z₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>h : p ≠ 0<GOAL>(Function.swap dslope z₀)^[p.order] f z₀ ≠ 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<GOAL>∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ p.order • (Function.swap dslope z₀)^[p.order] f z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>h : p ≠ 0<GOAL>∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<GOAL>(∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ↔ p = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<GOAL>(∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<VAR>hg : AnalyticAt 𝕜 g z₀<GOAL>(∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ g z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>w : 𝕜<VAR>hf : AnalyticAt 𝕜 f w<GOAL>(∃ᶠ (z : 𝕜) in 𝓝[≠] w, f z = 0) ↔ ∀ᶠ (z : 𝕜) in 𝓝 w, f z = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<VAR>hg : AnalyticAt 𝕜 g z₀<GOAL>(∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<GOAL>m = n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>m n : ℕ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z<GOAL>m = n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<GOAL>(∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<GOAL>hf.order = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<VAR>n : ℕ<GOAL>hf.order = ↑n ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>h₀ : z₀ ∈ U<VAR>hfw : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0<GOAL>Set.EqOn f 0 U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>z₀ : 𝕜<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<VAR>hU : IsPreconnected U<VAR>h₀ : z₀ ∈ U<VAR>hfz₀ : z₀ ∈ closure ({z | f z = 0} \ {z₀})<GOAL>Set.EqOn f 0 U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>z₀ : 𝕜<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>h₀ : z₀ ∈ U<VAR>hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z<GOAL>Set.EqOn f g U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>z₀ : 𝕜<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>h₀ : z₀ ∈ U<VAR>hfg : z₀ ∈ closure ({z | f z = g z} \ {z₀})<GOAL>Set.EqOn f g U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f g : 𝕜 → E<VAR>z₀ : 𝕜<VAR>ConnectedSpace 𝕜<VAR>hf : AnalyticOn 𝕜 f Set.univ<VAR>hg : AnalyticOn 𝕜 g Set.univ<VAR>hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z<GOAL>f = g
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>∃ C, 0 < C ∧ ∀ (v : V), C * ‖v‖ ≤ ‖(InnerProductSpace.continuousLinearMapOfBilin B) v‖
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>∃ C, 0 < C ∧ AntilipschitzWith C ⇑(InnerProductSpace.continuousLinearMapOfBilin B)
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>LinearMap.ker (InnerProductSpace.continuousLinearMapOfBilin B) = ⊥
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>IsClosed ↑(LinearMap.range (InnerProductSpace.continuousLinearMapOfBilin B))
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>LinearMap.range (InnerProductSpace.continuousLinearMapOfBilin B) = ⊤
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>v w : V<GOAL>⟪coercive.continuousLinearEquivOfBilin v, w⟫_ℝ = (B v) w
<VAR>V : Type u<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>v f : V<VAR>is_lax_milgram : ∀ (w : V), ⟪f, w⟫_ℝ = (B v) w<GOAL>f = coercive.continuousLinearEquivOfBilin v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<VAR>h : ∀ (x : E) (y : F), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜<GOAL>A = B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>A B : E →WOT[𝕜]F<GOAL>A = B ↔ ∀ (x : E) (y : F), ⟪y, A x⟫_𝕜 = ⟪y, B x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → E →WOT[𝕜]F<VAR>A : E →WOT[𝕜]F<GOAL>Filter.Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F), Filter.Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>RCLike 𝕜<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module 𝕜 E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>l : Filter (E →WOT[𝕜]F)<VAR>A : E →WOT[𝕜]F<GOAL>l ≤ 𝓝 A ↔ ∀ (x : E) (y : F), Filter.map (fun T => ⟪y, T x⟫_𝕜) l ≤ 𝓝 ⟪y, A x⟫_𝕜
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT s i n
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<VAR>m : ℕ<VAR>hm : m < MeasureTheory.SignedMeasure.findExistsOneDivLT s i<GOAL>¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i ∧ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i) ∧ 1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<GOAL>MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i j : Set α<GOAL>MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ j) ⊆ i
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<GOAL>MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<GOAL>1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) < ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>n : ℕ<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n.succ = MeasureTheory.SignedMeasure.someExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>n : ℕ<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n ⊆ i
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>n : ℕ<VAR>hn : ¬MeasureTheory.VectorMeasure.restrict s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤ MeasureTheory.VectorMeasure.restrict 0 (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<GOAL>1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s (i \ ⋃ k, ⋃ (_ : k ≤ n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)) + 1) < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i n.succ)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi₂ : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i<VAR>n : ℕ<VAR>hn : ¬MeasureTheory.VectorMeasure.restrict s (i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k) ≤ MeasureTheory.VectorMeasure.restrict 0 (i \ ⋃ k, ⋃ (_ : k < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i k)<GOAL>0 < ↑s (MeasureTheory.SignedMeasure.restrictNonposSeq s i n)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>n : ℕ<GOAL>MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i n)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>n m : ℕ<VAR>h : n < m<GOAL>MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<GOAL>Pairwise (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi₁ : MeasurableSet i<VAR>hi₂ : ↑s i < 0<VAR>hn : ¬∀ (n : ℕ), ¬MeasureTheory.VectorMeasure.restrict s (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l) ≤ MeasureTheory.VectorMeasure.restrict 0 (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq s i l)<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ ↑s j < 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i : Set α<VAR>hi : ↑s i < 0<GOAL>∃ j, MeasurableSet j ∧ j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ ↑s j < 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>0 ∈ s.measureOfNegatives
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>BddBelow s.measureOfNegatives
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>∃ i, MeasurableSet i ∧ MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<GOAL>∃ i j, MeasurableSet i ∧ MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasurableSet j ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ IsCompl i j
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>s : MeasureTheory.SignedMeasure α<VAR>i j : Set α<VAR>hi : MeasurableSet i<VAR>hj : MeasurableSet j<VAR>hi' : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧ MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ<VAR>hj' : MeasureTheory.VectorMeasure.restrict 0 j ≤ MeasureTheory.VectorMeasure.restrict s j ∧ MeasureTheory.VectorMeasure.restrict s jᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 jᶜ<GOAL>↑s (symmDiff i j) = 0 ∧ ↑s (symmDiff iᶜ jᶜ) = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E →ₗ[𝕜] E<VAR>hf : LipschitzWith 1 ⇑f<VAR>g : E →L[𝕜] ↥(LinearMap.eqLocus f 1)<VAR>hg_proj : ∀ (x : ↥(LinearMap.eqLocus f 1)), g ↑x = x<VAR>hg_ker : ↑(LinearMap.ker g) ⊆ closure ↑(LinearMap.range (f - 1))<VAR>x : E<GOAL>Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) id x_1 x) Filter.atTop (𝓝 ↑(g x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>f : E →L[𝕜] E<VAR>hf : ‖f‖ ≤ 1<VAR>x : E<GOAL>Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) id x_1 x) Filter.atTop (𝓝 ↑((orthogonalProjection (LinearMap.eqLocus f 1)) x))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>v : E<VAR>hv : v ∈ (Module.End.eigenspace T μ)ᗮ<GOAL>T v ∈ (Module.End.eigenspace T μ)ᗮ
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>hμ : Module.End.HasEigenvalue T μ<GOAL>(starRingEnd 𝕜) μ = μ
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>OrthogonalFamily 𝕜 (fun μ => ↥(Module.End.eigenspace T μ)) fun μ => (Module.End.eigenspace T μ).subtypeₗᵢ
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>OrthogonalFamily 𝕜 (fun μ => ↥(Module.End.eigenspace T (↑T μ))) fun μ => (Module.End.eigenspace T (↑T μ)).subtypeₗᵢ