[Merged by Bors] - feat(NumberTheory/Padics): Mahler coeffs tend to 0#19340
[Merged by Bors] - feat(NumberTheory/Padics): Mahler coeffs tend to 0#19340
Conversation
PR summary a6a94272cf
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.NumberTheory.Padics.MahlerBasis | 1632 | 1633 | +1 (+0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.NumberTheory.Padics.MahlerBasis |
1 |
Declarations diff
+ IsUltrametricDist.norm_fwdDiff_iter_apply_le
+ fwdDiff_iter_le_of_forall_le
+ fwdDiff_tendsto_zero
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
This adds the key technical lemma in the proof of Mahler's theorem characterising continuous functions on Zp: for any continuous function, the iterated forward differences at 0 tend to zero. Co-authored-by: Giulio Caflisch <gcaflisch@student.ethz.ch>
|
Build failed: |
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks for the PR! It generally looks like you could use calc more in order to make your proofs more readable and robust.
| · exact div_le_div_of_nonneg_left (norm_nonneg _) | ||
| (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk) |
There was a problem hiding this comment.
| · exact div_le_div_of_nonneg_left (norm_nonneg _) | |
| (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk) | |
| · gcongr |
Hopefully, this Just Works
There was a problem hiding this comment.
This doesn't work, and it remains broken even with the modification you subsequently proposed. So I am reverting it to the old code – which may not be as elegant, but actually does "just work".
| rw [← Int.cast_smul_eq_zsmul ℚ_[p], norm_smul] | ||
| refine le_trans ?_ (hst (i + ↑(p ^ t)) i ?_) | ||
| · apply mul_le_of_le_one_left (norm_nonneg _) | ||
| simpa only [← coe_intCast] using norm_le_one _ | ||
| · rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast] |
There was a problem hiding this comment.
This proof block looks like a good candidate for a calc
There was a problem hiding this comment.
The code that's here works fine and has already been submitted for merging by a maintainer (failing to merge only because of a coincidental rename of a lemma).
Can you explain why you believe all of these changes are so essential?
There was a problem hiding this comment.
The proof is now calc-ified. I don't personally think it makes it any clearer, but it's not worth arguing over.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
Looks like one of these Just Doesn’t Work (tm) |
|
Oh, you will need to add the assumption |
This adds the key technical lemma in the proof of Mahler's theorem characterising continuous functions on Zp: for any continuous function, the iterated forward differences at 0 tend to zero. Co-authored-by: Giulio Caflisch <gcaflisch@student.ethz.ch>
|
Pull request successfully merged into master. Build succeeded: |
This adds the key technical lemma in the proof of Mahler's theorem characterising continuous functions on Zp: for any continuous function, the iterated forward differences at 0 tend to zero.
Co-authored-by: Giulio Caflisch gcaflisch@student.ethz.ch