[Merged by Bors] - feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem#16797
[Merged by Bors] - feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem#16797Command-Master wants to merge 142 commits intomasterfrom
Conversation
Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
!bench |
|
Here are the benchmark results for commit e74605f. |
|
!bench |
1 similar comment
|
!bench |
|
Here are the benchmark results for commit 56e4164. Benchmark Metric Change
===============================================================
- ~Mathlib.FieldTheory.Differential.Basic instructions 169.6% |
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
|
The only point that bothers me is that the assumptions of the kind |
It works in |
| written in that way with `v, cᵢ, uᵢ ∈ F`. | ||
| -/ | ||
| class IsLiouville : Prop where | ||
| isLiouville (a : F) (ι : Type) [Fintype ι] (c : ι → F) (hc : ∀ x, (c x)′ = 0) |
There was a problem hiding this comment.
Should this be (c : ι → K), with K instead of F?
Or does that not matter?
Also, would you mind using different symbols in the conclusion, instead of c', u', v'. It looks a bit too much like the differential, eg in (c x)'.
Maybe c_0, u_0, v_0 instead?
There was a problem hiding this comment.
In Liouville's theorem we have a shared field of constants, so it doesn't matter. I don't know if this definition is useful in other cases, and what's the appropriate range in that case
There was a problem hiding this comment.
I'll use different symbols, but note that the differential uses ′, not ' - github simply displays them the same way in code blocks
|
Thanks 🎉 bors merge |
… Liouville's theorem (#16797) Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
… Liouville's theorem (#16797) Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>
* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...
mapCoeffson a differential ring #14967