Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - refactor(analysis/analytic/basic): redefine formal_multilinear_series.radius #5349

Closed
wants to merge 33 commits into from
Closed

[Merged by Bors] - refactor(analysis/analytic/basic): redefine formal_multilinear_series.radius #5349

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
9d83de1
chore(analysis/calculus): move the definition of `formal_multilinear_…
urkud Dec 13, 2020
3262bae
Long line
urkud Dec 13, 2020
244409a
refactor(analysis/analytic/basic): redefine `formal_multilinear_serie…
urkud Dec 13, 2020
7acd3e0
stash
urkud Dec 15, 2020
40b9757
Snapshot
urkud Dec 22, 2020
96498ac
Merge branch 'master' into lt-geom-tfae
urkud Dec 22, 2020
9e4ae59
Snapshot
urkud Dec 22, 2020
94a88a4
Merge branch 'lt-geom-tfae' into redefine-conv-radius
urkud Dec 22, 2020
1b6791a
Snapshot
urkud Dec 23, 2020
abb820f
Merge branch 'master' into lt-geom-tfae
urkud Dec 23, 2020
2fc2c88
Merge branch 'lt-geom-tfae' into redefine-conv-radius
urkud Dec 23, 2020
82a332b
Revert
urkud Dec 23, 2020
5766d19
Snapshot
urkud Dec 23, 2020
bd9fc8a
Merge branch 'master' into redefine-conv-radius
urkud Dec 25, 2020
9892b32
Merge branch 'lt-geom-tfae2' into redefine-conv-radius
urkud Dec 25, 2020
ad93b18
Merge branch 'master' into lt-geom-tfae2
urkud Dec 25, 2020
85f2356
Merge branch 'lt-geom-tfae2' into redefine-conv-radius
urkud Dec 25, 2020
06e7c0b
Snapshot
urkud Dec 25, 2020
77ff22c
Merge branch 'master' into redefine-conv-radius
urkud Dec 26, 2020
70f51ac
Fix file name
urkud Dec 26, 2020
25ac36c
Snapshot
urkud Dec 30, 2020
c77df1a
Merge branch 'master' into redefine-conv-radius
urkud Dec 30, 2020
5e73c4d
chore(data/real/{e,}nnreal): a few lemmas
urkud Dec 30, 2020
44076bc
Merge branch 'le-of-forall' into redefine-conv-radius
urkud Dec 30, 2020
17eef77
Snapshot
urkud Dec 30, 2020
34ca02f
chore(analysis/normed_space/basic): a few lemmas about `nnnorm`
urkud Dec 30, 2020
c6bae49
Fix
urkud Dec 30, 2020
bc3147b
Merge branch 'master' into redefine-conv-radius
urkud Dec 30, 2020
74efa48
Merge branch 'nnnorm-lemmas' into redefine-conv-radius
urkud Dec 30, 2020
dfad43e
Merge branch 'tsum-mul' into redefine-conv-radius
urkud Dec 30, 2020
49e9319
Merge branch 'master' into redefine-conv-radius
urkud Dec 30, 2020
7a9440f
Fix docs
urkud Dec 30, 2020
add0dd2
Update src/analysis/specific_limits.lean
urkud Dec 31, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 0 additions & 1 deletion src/algebra/big_operators/order.lean
View file
Open in desktop
Expand Up @@ -245,7 +245,6 @@ prod_induction f (λ x, 0 ≤ x) (λ _ _ ha hb, mul_nonneg ha hb) zero_le_one h0
lemma prod_pos {s : finset α} {f : α → β} (h0 : ∀(x ∈ s), 0 < f x) : 0 < (∏ x in s, f x) :=
prod_induction f (λ x, 0 < x) (λ _ _ ha hb, mul_pos ha hb) zero_lt_one h0


/- this is also true for a ordered commutative multiplicative monoid -/
lemma prod_le_prod {s : finset α} {f g : α → β} (h0 : ∀(x ∈ s), 0 ≤ f x)
(h1 : ∀(x ∈ s), f x ≤ g x) : (∏ x in s, f x) ≤ (∏ x in s, g x) :=
Expand Down