ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ N, ∀ {i : ℕ}, i ≥ N → ‖soln_gen hnorm - ↑(newton_cau_seq hnorm) i‖ < ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>‖Polynomial.eval (soln_gen hnorm) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>Filter.Tendsto (fun i => ‖Polynomial.eval (↑(newton_cau_seq hnorm) i) F‖) Filter.atTop (𝓝 0)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>Filter.Tendsto (fun n => ‖↑(newton_cau_seq hnorm) n - a‖) Filter.atTop (𝓝 (‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖))
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>Filter.Tendsto (fun n => ‖↑(newton_cau_seq hnorm) n - a‖) Filter.atTop (𝓝 ‖soln_gen hnorm - a‖)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>‖soln_gen hnorm - a‖ = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>‖soln_gen hnorm - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>Polynomial.eval (soln_gen hnorm) F = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>z : ℤ_[p]<VAR>hev : Polynomial.eval z F = 0<VAR>hnlt : ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<GOAL>z = soln_gen hnorm
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>ha : Polynomial.eval a F = 0<VAR>z' : ℤ_[p]<VAR>hz' : Polynomial.eval z' F = 0<VAR>hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖<GOAL>z' = a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>ha : Polynomial.eval a F = 0<GOAL>Polynomial.eval a F = 0 ∧ ‖a - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ‖Polynomial.eval a (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = a
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<GOAL>∃ z, Polynomial.eval z F = 0 ∧ ‖z - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ‖Polynomial.eval z (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖ ∧ ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ → z' = z
<VAR>G H : Type u<VAR>Monoid G<VAR>MulAction G H<VAR>g : G<VAR>x : H<GOAL>(Action.ofMulAction G H).ρ g x = g • x
<VAR>G : Type u<VAR>Monoid G<GOAL>(Action.leftRegular G).V = G
<VAR>G : Type u<VAR>Monoid G<GOAL>∀ (x : ↑(MonCat.of G)) (x_1 : G), (Action.leftRegular G).ρ x x_1 = x * x_1
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<GOAL>∀ (x : ↑(MonCat.of G)) (x_1 : Fin n → G) (a : Fin n), (Action.diagonal G n).ρ x x_1 a = (x • x_1) a
<VAR>G : Type u<VAR>Monoid G<VAR>n : ℕ<GOAL>(Action.diagonal G n).V = (Fin n → G)
<VAR>G : Type u<VAR>H : FintypeCat<VAR>Monoid G<VAR>MulAction G ↑H<VAR>g : G<VAR>x : ↑H<GOAL>(Action.FintypeCat.ofMulAction G H).ρ g x = g • x
<VAR>n : ℕ<VAR>s : ℝ<GOAL>0 ≤ ZetaAsymptotics.term n s
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>IntervalIntegrable (fun x => (x - ↑n) / x ^ (s + 1)) MeasureTheory.volume (↑n) (↑n + 1)
<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>ZetaAsymptotics.term n 1 = Real.log (↑n + 1) - Real.log ↑n - 1 / (↑n + 1)
<VAR>N : ℕ<GOAL>ZetaAsymptotics.term_sum 1 N = Real.log (↑N + 1) - ↑(harmonic (N + 1)) + 1
<GOAL>HasSum (fun n => ZetaAsymptotics.term (n + 1) 1) (1 - γ)
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>ZetaAsymptotics.term n s = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
<VAR>N : ℕ<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>ZetaAsymptotics.term_sum s N = 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>ZetaAsymptotics.term_tsum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s
<VAR>s : ℝ<VAR>hs : 1 < s<GOAL>∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * ZetaAsymptotics.term_tsum s
<VAR>n : ℕ<GOAL>ContinuousOn (fun x => ZetaAsymptotics.term (n + 1) x) (Set.Ici 1)
<GOAL>ContinuousOn ZetaAsymptotics.term_tsum (Set.Ici 1)
<GOAL>Filter.Tendsto (fun s => riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)
<GOAL>Filter.Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 ↑γ)
<VAR>F : Type u_1<VAR>Norm F<VAR>One F<VAR>NormOneClass F<GOAL>(fun s => riemannZeta s - 1 / (s - 1)) =O[𝓝 1] fun x => 1
<GOAL>Filter.Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
<GOAL>Filter.Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))
<GOAL>completedRiemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : ¬f ≈ 0<GOAL>∃ N, ∀ (m n : ℕ), N ≤ m → N ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>m n : ℕ<GOAL>PadicSeq.stationaryPoint hf ≤ m → PadicSeq.stationaryPoint hf ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<GOAL>f.norm = 0 ↔ f ≈ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<VAR>hf : f ≈ 0<GOAL>g ≈ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<GOAL>f.norm ≠ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<GOAL>∃ k, f.norm = padicNorm p k ∧ k ≠ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>¬(CauSeq.const (padicNorm p) q).LimZero
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q ≠ 0<GOAL>¬CauSeq.const (padicNorm p) q ≈ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<GOAL>0 ≤ f.norm
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v2 v3 : ℕ<GOAL>padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max (PadicSeq.stationaryPoint hf) (max v2 v3)))
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v3 : ℕ<GOAL>padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (PadicSeq.stationaryPoint hf) v3)))
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>v1 v2 : ℕ<GOAL>padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (PadicSeq.stationaryPoint hf))))
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<GOAL>f.norm = ↑p ^ (-f.valuation)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>f.valuation = g.valuation ↔ f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<GOAL>(f * g).norm = f.norm * g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : PadicSeq p<GOAL>CauSeq.Completion.mk f = 0 ↔ f ≈ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : PadicSeq p<GOAL>CauSeq.Completion.mk f ≠ 0 ↔ ¬f ≈ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<GOAL>PadicSeq.norm (CauSeq.const (padicNorm p) q) = padicNorm p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>PadicSeq.norm 1 = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<VAR>h : padicNorm p (↑f (PadicSeq.stationaryPoint hf)) ≠ padicNorm p (↑g (PadicSeq.stationaryPoint hg))<VAR>hlt : padicNorm p (↑g (PadicSeq.stationaryPoint hg)) < padicNorm p (↑f (PadicSeq.stationaryPoint hf))<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<VAR>hfg : f ≈ g<GOAL>padicNorm p (↑f (PadicSeq.stationaryPoint hf)) = padicNorm p (↑g (PadicSeq.stationaryPoint hg))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : f ≈ g<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfg : ¬f + g ≈ 0<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<GOAL>(f + g).norm ≤ max f.norm g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : PadicSeq p<GOAL>(-a).norm = a.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : f + g ≈ 0<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hfgne : f.norm ≠ g.norm<GOAL>(f + g).norm = max f.norm g.norm
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>0 = ⟦0⟧
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f g : PadicSeq p<GOAL>Padic.mk f = Padic.mk g ↔ f ≈ g
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>CauSeq.const (padicNorm p) q ≈ CauSeq.const (padicNorm p) r ↔ q = r
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q r : ℚ<GOAL>↑q = ↑r ↔ q = r
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ℚ<GOAL>↑(x + y) = ↑x + ↑y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ℚ<GOAL>↑(-x) = -↑x
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ℚ<GOAL>↑(x * y) = ↑x * ↑y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ℚ<GOAL>↑(x - y) = ↑x - ↑y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ℚ<GOAL>↑(x / y) = ↑x / ↑y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<GOAL>padicNormE (q + r) ≤ max (padicNormE q) (padicNormE r)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<GOAL>padicNormE q ≠ padicNormE r → padicNormE (q + r) = max (padicNormE q) (padicNormE r)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ<GOAL>padicNormE ↑q = padicNorm p q
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ_[p]<GOAL>q ≠ 0 → ∃ n, padicNormE q = ↑p ^ (-n)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ_[p]<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ r, padicNormE (q - ↑r) < ε
<VAR>n : ℕ<GOAL>0 < 1 / (↑n + 1)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ N, ∀ i ≥ N, padicNormE (↑f i - ↑(Padic.limSeq f i)) < ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<GOAL>IsCauSeq (padicNorm p) (Padic.limSeq f)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<GOAL>∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (q - ↑f i) < ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<GOAL>∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q : ℚ_[p]<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ r, ‖q - ↑r‖ < ε
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ_[p]<GOAL>↑(padicNormE q) = ‖q‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<GOAL>‖q + r‖ ≤ max ‖q‖ ‖r‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ_[p]<VAR>h : ‖q‖ ≠ ‖r‖<GOAL>‖q + r‖ = max ‖q‖ ‖r‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<GOAL>‖↑q‖ = ↑(padicNorm p q)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ_[p]<GOAL>q ≠ 0 → ∃ n, ‖q‖ = ↑(↑p ^ (-n))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ_[p]<GOAL>∃ q', ‖q‖ = ↑q'
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ_[p]<GOAL>‖q‖ = ↑(padicNormE.ratNorm q)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<GOAL>¬p ∣ q.den → ‖↑q‖ ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<GOAL>‖↑z‖ ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℚ_[p]<VAR>h : ‖z1 + z2‖ < ‖z2‖<GOAL>‖z1‖ = ‖z2‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℚ_[p]<VAR>h : ‖z1 + z2‖ < ‖z1‖<GOAL>‖z1‖ = ‖z2‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Padic.valuation 0 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Padic.valuation 1 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<VAR>hxy : x + y ≠ 0<GOAL>min x.valuation y.valuation ≤ (x + y).valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Padic.addValuationDef 0 = ⊤
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>Padic.addValuationDef 1 = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<GOAL>(x * y).addValuationDef = x.addValuationDef + y.addValuationDef
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<GOAL>min x.addValuationDef y.addValuationDef ≤ (x + y).addValuationDef
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>hx : x ≠ 0<GOAL>Padic.addValuation x = ↑x.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<GOAL>‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>DecidableEq α<VAR>DecidableEq β<VAR>v : β → ℤ<VAR>hv : v ∈ Finset.Icc 0 fun x => ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊<GOAL>A *ᵥ v ∈ Finset.Icc (fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * -(A i j)⁻) fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * (A i j)⁺
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>DecidableEq β<GOAL>(Finset.Icc 0 fun x => ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊).card = (⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ + 1) ^ Fintype.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>i : α<GOAL>(fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * -(A i j)⁻) i ≤ (fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * (A i j)⁺) i + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>DecidableEq α<GOAL>↑(Finset.Icc (fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * -(A i j)⁻) fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * (A i j)⁺).card = ∏ i : α, ((fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * (A i j)⁺) i - (fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * -(A i j)⁻) i + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>hA : A ≠ 0<GOAL>1 ≤ ‖A‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>hn : Fintype.card α < Fintype.card β<VAR>hm : 0 < Fintype.card α<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>(Finset.Icc (fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * -(A i j)⁻) fun i => ∑ j : β, ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊ * (A i j)⁺).card < (Finset.Icc 0 fun x => ↑⌊(↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))⌋₊).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>hn : Fintype.card α < Fintype.card β<VAR>hm : 0 < Fintype.card α<GOAL>∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑(Fintype.card β) * max 1 ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>A : Matrix α β ℤ<VAR>hn : Fintype.card α < Fintype.card β<VAR>hm : 0 < Fintype.card α<VAR>hA : A ≠ 0<GOAL>∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑(Fintype.card β) * ‖A‖) ^ (↑(Fintype.card α) / (↑(Fintype.card β) - ↑(Fintype.card α)))
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>x : K<GOAL>(NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodyLT K f ↔ ∀ (w : NumberField.InfinitePlace K), w x < ↑(f w)
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ NumberField.mixedEmbedding.convexBodyLT K f<GOAL>-x ∈ NumberField.mixedEmbedding.convexBodyLT K f
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<GOAL>Convex ℝ (NumberField.mixedEmbedding.convexBodyLT K f)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>NumberField.mixedEmbedding.convexBodyLTFactor K ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>1 ≤ NumberField.mixedEmbedding.convexBodyLTFactor K
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>NumberField K<GOAL>MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) = ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑(∏ w : NumberField.InfinitePlace K, f w ^ w.mult)
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<VAR>B : NNReal<VAR>hf : ∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → f w ≠ 0<GOAL>∃ g, (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : NumberField.InfinitePlace K, g w ^ w.mult = B
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>w₀ : { w // w.IsComplex }<VAR>x : K<GOAL>(NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀ ↔ (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧ |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>w₀ : { w // w.IsComplex }<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀<GOAL>-x ∈ NumberField.mixedEmbedding.convexBodyLT' K f w₀
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>w₀ : { w // w.IsComplex }<GOAL>Convex ℝ (NumberField.mixedEmbedding.convexBodyLT' K f w₀)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>NumberField.mixedEmbedding.convexBodyLT'Factor K ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>1 ≤ NumberField.mixedEmbedding.convexBodyLT'Factor K
<VAR>K : Type u_1<VAR>Field K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>w₀ : { w // w.IsComplex }<VAR>NumberField K<GOAL>MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀) = ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑(∏ w : NumberField.InfinitePlace K, f w ^ w.mult)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.convexBodySumFun x = ∑ w : NumberField.InfinitePlace K, ↑w.mult * (NumberField.mixedEmbedding.normAtPlace w) x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.convexBodySumFun x = ∑ w : { w // w.IsReal }, ‖x.1 w‖ + 2 * ∑ w : { w // w.IsComplex }, ‖x.2 w‖
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>0 ≤ NumberField.mixedEmbedding.convexBodySumFun x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.convexBodySumFun (-x) = NumberField.mixedEmbedding.convexBodySumFun x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x y : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.convexBodySumFun (x + y) ≤ NumberField.mixedEmbedding.convexBodySumFun x + NumberField.mixedEmbedding.convexBodySumFun y
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>c : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.convexBodySumFun (c • x) = |c| * NumberField.mixedEmbedding.convexBodySumFun x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>NumberField.mixedEmbedding.convexBodySumFun x = 0 ↔ x = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>‖x‖ ≤ NumberField.mixedEmbedding.convexBodySumFun x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Continuous NumberField.mixedEmbedding.convexBodySumFun
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<VAR>hB : B ≤ 0<GOAL>MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) = 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<VAR>x : K<GOAL>(NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodySum K B ↔ ∑ w : NumberField.InfinitePlace K, ↑w.mult * ↑w x ≤ B
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ NumberField.mixedEmbedding.convexBodySum K B<GOAL>-x ∈ NumberField.mixedEmbedding.convexBodySum K B
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<GOAL>Convex ℝ (NumberField.mixedEmbedding.convexBodySum K B)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<GOAL>Bornology.IsBounded (NumberField.mixedEmbedding.convexBodySum K B)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<GOAL>IsCompact (NumberField.mixedEmbedding.convexBodySum K B)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>NumberField.mixedEmbedding.convexBodySumFactor K ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>B : ℝ<GOAL>MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) = ↑(NumberField.mixedEmbedding.convexBodySumFactor K) * ENNReal.ofReal B ^ FiniteDimensional.finrank ℚ K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<GOAL>MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I)) = ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<GOAL>NumberField.mixedEmbedding.minkowskiBound K I < ⊤
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<GOAL>0 < NumberField.mixedEmbedding.minkowskiBound K I
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>h : NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(f w)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>f : NumberField.InfinitePlace K → NNReal<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<VAR>w₀ : { w // w.IsComplex }<VAR>h : NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀)<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ ↑w₀ → w a < ↑(f w)) ∧ |((↑w₀).embedding a).re| < 1 ∧ |((↑w₀).embedding a).im| < ↑(f ↑w₀) ^ 2