padicNormE.mul
theorem padicNormE.mul : ∀ {p : ℕ} [hp : Fact p.Prime] (q r : ℚ_[p]), ‖q * r‖ = ‖q‖ * ‖r‖
This theorem states that for any natural number `p` which is prime, and any two p-adic numbers `q` and `r`, the p-adic norm of the product of `q` and `r` is equal to the product of the p-adic norms of `q` and `r`. In mathematical notation, this could be written as `‖q * r‖ = ‖q‖ * ‖r‖`. This theorem essentially states that the p-adic norm is multiplicative.
More concisely: For any prime natural number p and p-adic numbers q and r, the p-adic norm of their product equals the product of their individual p-adic norms: ‖q * r‖ = ‖q‖ * ‖r‖.
|
padicNormE.add_eq_max_of_ne'
theorem padicNormE.add_eq_max_of_ne' :
∀ {p : ℕ} [inst : Fact p.Prime] {q r : ℚ_[p]},
padicNormE q ≠ padicNormE r → padicNormE (q + r) = max (padicNormE q) (padicNormE r)
This theorem states that for any prime number `p` and any two elements `q` and `r` in the `p`-adic numbers, if the `p`-adic norms of `q` and `r` are not equal, then the `p`-adic norm of the sum of `q` and `r` is equal to the maximum of the `p`-adic norms of `q` and `r`. The `p`-adic norm is a function that assigns a rational number to each `p`-adic number, based on the norm on Cauchy sequences, and is denoted by `padicNormE`. The theorem is named with a `'` to avoid name conflicts with equivalent theorems about the standard norm.
More concisely: For any prime number `p` and `p`-adic numbers `q` and `r`, if `padicNormE q ≠ padicNormE r`, then `padicNormE (q + r) = max (padicNormE q) (padicNormE r)`.
|
Padic.norm_eq_pow_val
theorem Padic.norm_eq_pow_val : ∀ {p : ℕ} [hp : Fact p.Prime] {x : ℚ_[p]}, x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)
This theorem, named `Padic.norm_eq_pow_val`, states that for any non-zero rational number `x` in the `p`-adic number field `ℚ_[p]` (where `p` is a prime number), the `p`-adic norm of `x` (denoted by `‖x‖`) is equal to `p` raised to the power of the negative `p`-adic valuation of `x`. This implies a connection between the `p`-adic norm and `p`-adic valuation of a `p`-adic number, reflecting a fundamental property of `p`-adic numbers.
More concisely: For any non-zero $p$-adic number $x$ in the field $\mathbb{Q}_p$, its $p$-adic norm $\|x\|$ equals $p^{-v_p(x)}$, where $v_p(x)$ is the $p$-adic valuation of $x$.
|
PadicSeq.stationaryPoint_spec
theorem PadicSeq.stationaryPoint_spec :
∀ {p : ℕ} [inst : Fact p.Prime] {f : PadicSeq p} (hf : ¬f ≈ 0) {m n : ℕ},
PadicSeq.stationaryPoint hf ≤ m → PadicSeq.stationaryPoint hf ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)
The theorem `PadicSeq.stationaryPoint_spec` states that for any prime number `p` and any `p`-adic Cauchy sequence `f` that is not equivalent to zero, if natural numbers `m` and `n` are greater than or equal to the stationary point of `f`, then the `p`-adic norm of `f` at the indices `m` and `n` is the same. In other words, beyond the stationary point of a `p`-adic Cauchy sequence, the `p`-adic norm remains constant.
More concisely: For any `p`-adic Cauchy sequence `f` that is not equivalent to zero, the `p`-adic norm of `f` at indices greater than or equal to its stationary point is constant.
|
PadicSeq.norm_zero_iff
theorem PadicSeq.norm_zero_iff : ∀ {p : ℕ} [inst : Fact p.Prime] (f : PadicSeq p), f.norm = 0 ↔ f ≈ 0
The theorem `PadicSeq.norm_zero_iff` states that for a prime number `p` and a Cauchy sequence of rational numbers `f` with respect to the p-adic norm, the norm of the sequence `f` is equal to 0 if and only if the sequence `f` is equivalent to 0. Here, a sequence is considered equivalent to 0 if its elements approach 0 as the sequence progresses. This theorem is crucial in analyzing the behavior of Cauchy sequences in p-adic number systems.
More concisely: For a prime number p and a Cauchy sequence of rational numbers f with respect to the p-adic norm, the sequence f has norm 0 if and only if it converges to 0.
|
Padic.rat_dense'
theorem Padic.rat_dense' : ∀ {p : ℕ} [inst : Fact p.Prime] (q : ℚ_[p]) {ε : ℚ}, 0 < ε → ∃ r, padicNormE (q - ↑r) < ε
This theorem, `Padic.rat_dense'`, states that for any prime number `p`, and for any element `q` in the `p`-adic numbers ℚ_[p] and any positive rational number `ε`, there exists a rational number `r` such that the `p`-adic norm of the difference between `q` and `r` is less than `ε`. In other words, the rational numbers are densely embedded within the `p`-adic numbers to any desired level of precision `ε`.
More concisely: For any prime number `p` and positive rational number `ε`, the `p`-adic numbers ℚ_[p] contain a rational number `r` with `p`-adic norm of the difference between `q` and `r` less than `ε` for any given `q` in ℚ_[p].
|
padicNormE.nonarchimedean
theorem padicNormE.nonarchimedean : ∀ {p : ℕ} [hp : Fact p.Prime] (q r : ℚ_[p]), ‖q + r‖ ≤ max ‖q‖ ‖r‖
The theorem `padicNormE.nonarchimedean` states that for every natural number `p` that is prime (denoted by `Nat.Prime p`), for every pair of p-adic numbers `q` and `r`, the p-adic norm (denoted by ‖.‖) of the sum of `q` and `r` is less than or equal to the maximum of their individual p-adic norms. In other words, in the p-adic number system, the norm of the sum of two numbers does not exceed the maximum of their individual norms, exhibiting a property of non-Archimedean fields.
More concisely: For every prime number p in the natural numbers, the p-adic norm of the sum of two p-adic numbers is less than or equal to the maximum of their individual p-adic norms.
|
PadicSeq.lift_index_right
theorem PadicSeq.lift_index_right :
∀ {p : ℕ} [inst : Fact p.Prime] {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v2 : ℕ),
padicNorm p (↑f (PadicSeq.stationaryPoint hf)) =
padicNorm p (↑f (max v1 (max v2 (PadicSeq.stationaryPoint hf))))
This theorem, named `PadicSeq.lift_index_right`, is about manipulating indices of a `p`-adic sequence, where `p` is a prime number. Specifically, for a given `p`-adic sequence `f` that is not equivalent to the zero sequence, and any two natural numbers `v1` and `v2`, the `p`-adic norm of the `f`th term at the stationary point of `f` is equal to the `p`-adic norm of the `f`th term at the maximum of `v1`, `v2`, and the stationary point of `f`. The stationary point of a `p`-adic sequence is such that beyond this point, the `p`-adic norm of all further terms in the sequence is constant. This theorem allows for flexibility in selecting the index of the `p`-adic sequence while still preserving the `p`-adic norm value.
More concisely: For any `p`-adic sequence `f` not equal to the zero sequence and natural numbers `v1`, `v2`, the `p`-adic norm of `f` at the maximum of `{v1, v2, stationary_point(f)}` equals the `p`-adic norm of `f` at the stationary point.
|
Padic.const_equiv
theorem Padic.const_equiv :
∀ (p : ℕ) [inst : Fact p.Prime] {q r : ℚ}, CauSeq.const (padicNorm p) q ≈ CauSeq.const (padicNorm p) r ↔ q = r := by
sorry
The theorem `Padic.const_equiv` states that for any natural number `p` that is prime, and any two rational numbers `q` and `r`, the Cauchy sequence constants determined by the `p`-adic norm of `q` and `r` are equivalent if and only if `q` equals `r`. In other words, two rational numbers are identical if their `p`-adic norm-based Cauchy sequence constants are equivalent. The `p`-adic norm of a rational number `q` is calculated as `p` to the power of negative `p`-adic valuation of `q` if `q` is not equal to zero, otherwise it is zero.
More concisely: For any prime number p and rational numbers q and r, the equivalence of their p-adic Cauchy sequence constants implies q = r.
|
padicNormE.norm_p
theorem padicNormE.norm_p : ∀ {p : ℕ} [hp : Fact p.Prime], ‖↑p‖ = (↑p)⁻¹
The theorem `padicNormE.norm_p` states that for any natural number `p` which is prime, the p-adic norm of `p`, denoted as `‖↑p‖`, equals the reciprocal of `p`, denoted as `(↑p)⁻¹`. In mathematical terms, this theorem asserts that the p-adic norm of a prime number is its inverse.
More concisely: The p-adic norm of a prime number p is equal to the reciprocal of p, i.e., ‖↑p‖ = (↑p)⁻¹.
|
PadicSeq.norm_equiv
theorem PadicSeq.norm_equiv : ∀ {p : ℕ} [hp : Fact p.Prime] {f g : PadicSeq p}, f ≈ g → f.norm = g.norm
The theorem `PadicSeq.norm_equiv` states that for any natural number `p` that is prime, and for any two `p`-adic Cauchy sequences `f` and `g`, if `f` and `g` are equivalent (i.e., the distance between `f` and `g` tends to zero), then the `p`-adic norms of `f` and `g` are equal. In other words, the process of taking the `p`-adic norm of a Cauchy sequence is well-defined up to equivalence of sequences.
More concisely: For any prime number `p`, if two `p`-adic Cauchy sequences are equivalent, then they have equal `p`-adic norms.
|
padicNormE.add_eq_max_of_ne
theorem padicNormE.add_eq_max_of_ne : ∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ_[p]}, ‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖
This theorem states that for any prime number `p`, and any two p-adic numbers `q` and `r`, if the p-adic norms of `q` and `r` are not equal, then the p-adic norm of the sum of `q` and `r` is equal to the maximum of the p-adic norms of `q` and `r`. Here, a p-adic number is a type of number that comes from a different number system than the one we typically use, and the p-adic norm of a p-adic number is a measure of the size of that number.
More concisely: For any prime number `p` and p-adic numbers `q` and `r`, if `|q|_p ≠ |r|_p`, then `|q + r|_p = max {|q|_p, |r|_p}`.
|
PadicSeq.lift_index_left_left
theorem PadicSeq.lift_index_left_left :
∀ {p : ℕ} [inst : Fact p.Prime] {f : PadicSeq p} (hf : ¬f ≈ 0) (v2 v3 : ℕ),
padicNorm p (↑f (PadicSeq.stationaryPoint hf)) =
padicNorm p (↑f (max (PadicSeq.stationaryPoint hf) (max v2 v3)))
The theorem `PadicSeq.lift_index_left_left` states that for every natural number `p` which is prime, and for a Cauchy sequence `f` of rationals with respect to the `p`-adic norm, if `f` is not equivalent to `0`, then the `p`-adic norm of the rational number represented by the sequence `f` at the stationary point `PadicSeq.stationaryPoint hf` is equal to the `p`-adic norm of the rational number represented by the sequence `f` at the maximum of the stationary point and the maximum of two given natural numbers `v2` and `v3`. The auxiliary lemma is useful for manipulating indices of sequences in `p`-adic number theory.
More concisely: For a prime number p and a Cauchy sequence f of rationals with respect to the p-adic norm that is not equivalent to 0, the p-adic norm of the sequence's limit equals the larger of the p-adic norms at the stationary point and the maximum of two given natural numbers v2 and v3.
|
padicNormE.eq_padicNorm
theorem padicNormE.eq_padicNorm : ∀ {p : ℕ} [hp : Fact p.Prime] (q : ℚ), ‖↑q‖ = ↑(padicNorm p q)
The theorem `padicNormE.eq_padicNorm` states that for any prime number `p` and any rational number `q`, the p-adic norm of `q`, denoted as `‖↑q‖`, is equal to the p-adic norm of `q` as defined by the function `padicNorm`. In other words, the p-adic norm of `q` under the standard p-adic norm function is the same as the p-adic norm of `q` under the `padicNorm` function when `p` is prime.
More concisely: For any prime number p and rational number q, the standard p-adic norm of q equals the p-adic norm of q computed by the `padicNorm` function.
|
PadicSeq.norm_nonneg
theorem PadicSeq.norm_nonneg : ∀ {p : ℕ} [inst : Fact p.Prime] (f : PadicSeq p), 0 ≤ f.norm
The theorem `PadicSeq.norm_nonneg` states that for any natural number `p`, given that `p` is prime, and for any sequence `f` of Cauchy sequences of rationals with respect to the `p`-adic norm, the norm of this sequence `f`, as calculated by the `PadicSeq.norm` function, is always nonnegative. In other words, the norm of a p-adic Cauchy sequence is always greater than or equal to zero.
More concisely: For any prime number `p` and any Cauchy sequence `f` of rationals with respect to the `p`-adic norm, `PadicSeq.norm f ≥ 0`.
|
PadicSeq.lift_index_left
theorem PadicSeq.lift_index_left :
∀ {p : ℕ} [inst : Fact p.Prime] {f : PadicSeq p} (hf : ¬f ≈ 0) (v1 v3 : ℕ),
padicNorm p (↑f (PadicSeq.stationaryPoint hf)) =
padicNorm p (↑f (max v1 (max (PadicSeq.stationaryPoint hf) v3)))
This theorem, titled "PadicSeq.lift_index_left", is an auxiliary lemma used for manipulation of sequence indices. It states that for any prime number `p`, and any given `p`-adic sequence `f` that does not vanish to zero, the `p`-adic norm of the stationary point of `f` is equal to the `p`-adic norm of the maximum value among `v1`, the stationary point of `f`, and `v3`. This theorem is essentially saying that if we lift the index to a larger value, the `p`-adic norm remains the same as the `p`-adic norm at the stationary point.
More concisely: For any prime number `p` and `p`-adic sequence `f` that does not vanish at its stationary point, the `p`-adic norm of the stationary point is equal to the `p`-adic norm of the maximum between the stationary point and any other point.
|
PadicSeq.stationary
theorem PadicSeq.stationary :
∀ {p : ℕ} [inst : Fact p.Prime] {f : CauSeq ℚ (padicNorm p)},
¬f ≈ 0 → ∃ N, ∀ (m n : ℕ), N ≤ m → N ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)
The theorem `PadicSeq.stationary` states that for a given prime number `p` and a nonzero Cauchy sequence `f` of rational numbers with respect to the `p`-adic norm, there exists a certain natural number `N`, such that for any pair of natural numbers `m` and `n` which are at least as large as `N`, the `p`-adic norm of the `n`-th and `m`-th terms of the sequence are equal. In essence, the `p`-adic norms of the terms of the sequence become constant after a certain point.
More concisely: For any prime number `p` and nonzero Cauchy sequence `f` of rational numbers with respect to the `p`-adic norm, there exists a natural number `N` such that for all `m, n >= N`, `|f(m) - f(n)|_p = 0`. (Here, `|.|_p` denotes the `p`-adic norm.)
|
padicNormE.nonarchimedean'
theorem padicNormE.nonarchimedean' :
∀ {p : ℕ} [inst : Fact p.Prime] (q r : ℚ_[p]), padicNormE (q + r) ≤ max (padicNormE q) (padicNormE r)
This theorem is about the `padicNormE` function and has a 'prime' in its name to avoid conflict with equivalent theorems about the standard norm function `‖ ‖`. Specifically, it's asserting a property known as non-Archimedean, which is a characteristic of certain mathematical spaces. In this case, given any prime number `p`, and any two elements `q` and `r` from the set of `p`-adic numbers `ℚ_[p]`, the `p`-adic norm of the sum of `q` and `r` is less than or equal to the maximum of the `p`-adic norms of `q` and `r`. In mathematical notation, it is saying that for all `p`, `q`, and `r`, we have `‖q + r‖_p ≤ max(‖q‖_p, ‖r‖_p)`.
More concisely: For any prime number `p`, the `p`-adic norm of the sum of two `p`-adic numbers is less than or equal to the maximum of their individual `p`-adic norms.
|