mathlib3
feat(analysis/locally_convex/with_seminorms): equicontinuity criterions
#17275
Open
Overview
Commits
257
Changes
View On GitHub

feat(analysis/locally_convex/with_seminorms): equicontinuity criterions #17275

ADedecker wants to merge 257 commits into master from AD_seminorm_equicontinuity
ADedecker
ADedecker Swap uniform inducing !
27381c67
ADedecker Pi swap part2
f047d043
ADedecker Remove exit
44668a10
ADedecker Small fix
807bd2e9
ADedecker Use notation
aef9e6ba
ADedecker First part done for đť”–-convergence
6daa5f9a
ADedecker Setup for precomp
cdb016ac
ADedecker Precomp uniform continuous
55a34852
ADedecker Finished ?
d0feed09
ADedecker Move things
0300426a
ADedecker Docs
1ef44602
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
87bb8ea5
ADedecker Begin
5ca6a994
ADedecker Content
e6e4892a
ADedecker Fix doc
59de0d7b
ADedecker Merge branch 'AD_uniform_equiv' into AD_uniform_convergence_comp2
3a25d791
ADedecker Small fix
33b3dbe1
ADedecker Fix
c269b680
ADedecker Merge branch 'AD_uniform_equiv' into AD_uniform_convergence_comp2
2aad376d
ADedecker Tmp (this won't compile)
6a674952
ADedecker Add Pi version of `arrow_prod_equiv_prod_arrow`
4b3afd9e
ADedecker Merge branch 'AD_Pi_arrow' into AD_uniform_convergence_comp2
f8c0b4a4
ADedecker Change approach
eaf4207f
ADedecker Merge branch 'AD_Pi_arrow' into AD_uniform_convergence_comp2
3624a818
ADedecker Use uniform_equiv
5ff68782
ADedecker Setup
807d7826
ADedecker Make phi explicit, suggestions from review
1dbd0fa8
ADedecker Remove useless restriction
0d5e837e
ADedecker Merge branch 'AD_uniform_equiv' into AD_uniform_convergence_comp2
e7afdd66
ADedecker Merge branch 'AD_Pi_arrow' into AD_uniform_convergence_comp2
ced2f8a4
ADedecker Fix; add congr and prod
52802675
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
5887bb91
ADedecker Fix
d947a723
ADedecker Def doc
e833ea0e
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
2f4a3c62
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
d147bb98
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
291f2d92
ADedecker Finished
6dc5ff11
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
08575d89
ADedecker Useless import
2ff69006
ADedecker Begin
a7d222bf
ADedecker Basis of directed [b]infi
c9b3c510
ADedecker Merge branch 'basis_infi_directed' into AD_uniform_convergence_bases
efcf83dd
ADedecker Bases for topology/uniform structure of đť”–-convergence
7d35d831
ADedecker Dedup
0c462936
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
d61aea07
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
e5516499
ADedecker Better parameters, lint failures
8f6658f5
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
5e84d30e
ADedecker Merge remote-tracking branch 'origin/AD_uniform_convergence_comp2' in…
0da793a2
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
63480fa6
PatrickMassot Minor tweaks
6cf69351
ADedecker Merge remote-tracking branch 'origin/AD_uniform_convergence_comp2' in…
6691df83
ADedecker Merge remote-tracking branch 'origin/AD_uniform_convergence_comp2' in…
65f5806b
ADedecker Fix
103aa36b
ADedecker Start writing more docs
e98a4d65
ADedecker Use notations
4b85b6e2
ADedecker More docs
99ae5ee0
ADedecker Lots of comments
f83d4da9
ADedecker Finish doc, add missing lemmas!
b40cd87f
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
a565cfde
ADedecker Merge branch 'AD_uniform_convergence_comp2' into AD_uniform_convergen…
37d6fd54
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
665c904c
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
0a3e8d38
ADedecker Fix and comments
0996aa17
ADedecker Better docstring and comments
56ddf8e5
YaelDillies initial commit
630b5624
YaelDillies kill nonneg'
58edc47e
YaelDillies typos
814520a3
YaelDillies fix analysis.seminorm
0b40898f
YaelDillies seminorm classes
8bc92fc5
YaelDillies group norms
e6eaa180
YaelDillies nolint
9c5fd521
YaelDillies Merge branch 'seminorm_class' into group_norm
3135af4a
YaelDillies kill cores
90aab8e9
YaelDillies fix analysis.normed_space.operator_norm
7d4b8702
YaelDillies fix analysis.normed_space.continuous_affine_map
ccd55198
YaelDillies fix analysis.inner_product_space.basic
629bf2c3
YaelDillies fix analysis.normed_space.lp_space
d1b8ac6e
YaelDillies fix measure_theory.function.lp_space
ee9738bc
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
a7b63d47
ADedecker Merge remote-tracking branch 'origin/master' into AD_uniform_converge…
b89ec73f
ADedecker Begin
e4902991
ADedecker Criterions
445b3c23
ADedecker Merge branch 'AD_uniform_convergence_bases' into AD_equicontinuous
adf7fc86
ADedecker Bump, bases
d26dcb40
ADedecker Test
f9fe1039
ADedecker Go back
e3b5bb92
ADedecker Go back again
ca094a23
ADedecker Let's do that later
16829165
ADedecker Progress
20d354e1
ADedecker Closure, finish fixing everything
085ebe3a
ADedecker Uniform equicontinuity on compact spaces
001cb51f
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
fba0c8d2
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
a4e661bd
ADedecker Docs
86f89e85
YaelDillies backport map_nonneg
0514687e
YaelDillies Merge remote-tracking branch 'origin/master' into kill_normed_group_core
b74d862a
YaelDillies bump
d1f7098e
ADedecker ++
ca1ec0ad
ADedecker Done
f80d9197
ADedecker Merge branch 'AD_uniform_convergence_group' into AD_group_equicontinuity
c8857efb
ADedecker Begin
49263b4e
YaelDillies whooops #lint
0080f108
ADedecker ofSupInf
75b09303
ADedecker Fix
17ee5051
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
9d80d077
ADedecker ++
08bc0980
ADedecker Remove exit
8ee0e6bd
ADedecker ++
ab3a65ac
ADedecker Docs
0ca2fd01
ADedecker Merge branch 'AD_seminorm_Sup' into AD_seminorm_equicontinuity
977a776d
ADedecker Faster
db9b3911
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_equicon…
5ccc5ddc
ADedecker Merge branch 'AD_seminorm_Sup' into AD_seminorm_equicontinuity
da5ab0ff
ADedecker ++
63f9d5ea
ADedecker Continuity modulus at a point
797c7ad0
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
b3610a75
YaelDillies Merge remote-tracking branch 'origin/master' into kill_normed_group_core
74521c0d
ADedecker Need Yael's code
ae1c772a
ADedecker Merge remote-tracking branch 'origin/kill_normed_group_core' into AD_…
77c2535e
YaelDillies fix analysis.complex.basic
0a298526
ADedecker ++
af9eed59
ADedecker Done
495d347c
ADedecker Merge remote-tracking branch 'origin/kill_normed_group_core' into AD_…
1bf96099
ADedecker Content
8c8d2253
ADedecker Merge branch 'AD_with_seminorms_iff_infi_norms' into AD_seminorm_equi…
e20a6f44
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
5a11ff1f
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
e6e2187d
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_equicon…
a41f5a62
ADedecker Merge remote-tracking branch 'origin/master' into AD_group_equicontin…
296e8d5c
ADedecker Small fixes
0bb30103
ADedecker Fix
c15b879b
ADedecker Fix'
ef9257ba
ADedecker Progress
9c5fa2e2
ADedecker Cleaner
b792fda3
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
46622578
ADedecker ++
fb8010bc
ADedecker ++
ac121fde
ADedecker Progress
e8a70b38
ADedecker Closed-ball characterization of continuity of a seminorm
36e9d8f5
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_seminorm_eq…
074f1ac0
ADedecker Step 1 done
343e1d8b
ADedecker 3-week-ago self was dumb
81e8979e
ADedecker Only hard part remaining
d53e327e
ADedecker Going to split
799b983c
ADedecker ADedecker added WIP
ADedecker ADedecker added t-analysis
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
ADedecker Fix stupid assumptions
3a27ee6c
ADedecker More related fixes
a6045f9a
ADedecker Initial commt
2b13f669
ADedecker Progress
22404975
ADedecker Switch to "one seminorm first" approach
57750f9b
ADedecker Done!
b36a4bb3
ADedecker Begin semilinearizing `comp`
79001fee
ADedecker Semilinearize `seminorm.comp`
58889133
ADedecker Merge branch 'AD_semilinearize_seminorm_comp' into AD_refactor_shell_…
a06746b3
ADedecker Docs
a3d41a23
ADedecker Closure of `{0}` in a seminormed group
0b39e399
ADedecker Merge branch 'AD_closure_one' into AD_refactor_shell_seminorms
222aab07
ADedecker Docstrings
7409f227
ADedecker ++
06988108
ADedecker Add mem lemma
d1a4b194
ADedecker Merge branch 'AD_closure_one' into AD_refactor_shell_seminorms
0b8967bc
ADedecker Progress
1465689d
ADedecker Swa)
7d57ec3d
ADedecker Merge branch 'AD_closure_one' into AD_refactor_shell_seminorms
63713e0c
ADedecker Fixes
046b0de0
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
9a07b887
ADedecker Suggestions from review
e2cc5b73
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_continu…
bf299e24
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
20ef121b
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_refactor_sh…
b9c59be4
ADedecker Merge remote-tracking branch 'origin/master' into AD_equicontinuous
93b1ace7
ADedecker Fix
6b5bf4f3
ADedecker Fixes again
78b49c50
ADedecker Move to new file (I'll write the docstring later)
cbc13830
ADedecker Eventually
f06e8227
ADedecker Add docstringd
8aa578a6
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
3f605b19
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
bb6b4147
ADedecker Add missing import
81c15ebb
ADedecker Remove now-useless import
78c19f78
ADedecker Proper module docstring
48f151b2
ADedecker Add comment about relative versions
7b7e9633
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
0cf9c5d0
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
b28d0d91
ADedecker to_additive
b6b4b642
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
b44bdc41
ADedecker Make linter happy
0bef1ecd
ADedecker Start
b20c412a
ADedecker Full test, part 1
cb9a9395
ADedecker ++
f89ac58f
ADedecker Update docstrings for first half of file
34b7305a
ADedecker Update dosctrings in second half of file
7b257abe
ADedecker Remove commented code
5b18a4f1
ADedecker Update module docstring
eb686f03
ADedecker Update docstrings in `topology/algebra/uniform_convergence`
c29b3a73
ADedecker Update `topology/algebra/module/strong_topology`
4d32b0ee
ADedecker Add TODO
c8a2db40
ADedecker Merge branch 'AD_uniform_continuous_type_alias' into AD_equicontinuous
550844c5
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
4793c504
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
4fcf0db0
ADedecker Fixes, part1
2a1a84d6
ADedecker All fixed?
d4e15837
ADedecker Merge remote-tracking branch 'origin/AD_equicontinuous' into AD_group…
3584afbb
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
eb4b1e8c
ADedecker Last fixes
457acd16
ADedecker Merge remote-tracking branch 'origin/AD_equicontinuous' into AD_group…
a893d47f
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
6e4259af
ADedecker Fixes
05ea2ce8
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
790854a4
ADedecker Fix again
0a41de15
ADedecker Merge remote-tracking branch 'origin/master' into AD_seminorm_continu…
0ed68d92
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
76dbdb53
ADedecker Fix
a419cb93
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_refactor_sh…
6b29a278
ADedecker Fix
688a8c67
ADedecker More norm breakage
fa4565a7
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
a4eb4f8e
ADedecker Fix Ascoli
81426cce
ADedecker Merge branch 'AD_equicontinuous' into AD_seminorm_equicontinuity
f60f857a
ADedecker Fix, comment dead code
d2c959d9
ADedecker Generalize radius
41ff1bee
ADedecker Eric's suggestions
3a87b89b
ADedecker Floris's sugestions
8dbbcc27
ADedecker Useless ()
53309d8d
ADedecker More variations for closure
7befa296
ADedecker Add a few more lemmas
001e3d4c
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
973de836
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
29cb7dda
ADedecker Fix again
a0621a70
ADedecker Merge branch 'AD_equicontinuous' into AD_group_equicontinuity
828c64fa
ADedecker Merge branch 'AD_group_equicontinuity' into AD_seminorm_equicontinuity
7104ea56
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
a058e58e
ADedecker Merge branch 'AD_seminorm_continuous_closed_ball' into AD_refactor_sh…
a62881a1
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
f36fbba4
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
75f95122
ADedecker Fix1
3f54becb
ADedecker ++
1ae42b61
ADedecker More fixes
1ac6cf57
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
24ec27d1
github-actions github-actions added modifies-synchronized-file
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
9a679c38
ADedecker Move things around
e9c4fade
ADedecker Add a todo
d1d57fd7
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
9743dab7
ADedecker Long line
68219f97
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
a71ea2d7
ADedecker Merge remote-tracking branch 'origin/master' into AD_refactor_shell_s…
362dc7b7
ADedecker Update src/analysis/locally_convex/with_seminorms.lean
5da63a98
ADedecker Fix comment
37837dc8
ADedecker Merge branch 'AD_refactor_shell_seminorms' into AD_seminorm_equiconti…
dbde88c8
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
WIP t-analysis modifies-synchronized-file too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum