mathlib3
feat(analysis/inner_product_space/trace_class): define the trace of a positive operator
#15451
Open
Open
feat(analysis/inner_product_space/trace_class): define the trace of a positive operator #15451
ADedecker
wants to merge
199 commits into
master
from
AD_trace_class_3
start refactor of std_orthonormal_basis
3d4264a8
+finsupp.dom_licongr
799645a9
inserted some lemmas, still working on reindex_apply
d5f5da76
add orthonormal_basis.reindex API
c751fd52
add equiv to and from euclidean_space
8e288c5b
add subordinate_orthonormal_basis
7a667b9b
cleanup
079f984b
small fixes involving to_eulidean_space
06596f6e
small changes involving of_euclidean_space
087404fc
delinting / fixing problems in orientation
03a37bae
delinting
eaad773b
Merge branch 'master' into std_orthonormal_basis
c698db51
is_self_adjoint.eigenvector is of type orthonormal_basis
0bedf21f
merging typo
585bf6e1
add std_orthonormal_basis to docstring
f30b8144
delinting in pi_Lp
5fce2d09
delint pi_L2
709a748d
fix for missing symm_trans_apply
a8156425
suggested changes to pi_L2
288a6d50
suggested changes to spectrum
64164cc2
suggested changes to pi_Lp
b63e9bcc
rewrite docstring
b8c6250f
fix curly braces and long lines
d9845efe
fixes relating to from_orthogonal_span_singleton
713d3844
fix sphere.lean
5f2a44ca
found 100+ character line
ed6c1133
fixed sphere, but in weird way
1023442e
add maximal_ortho... to make undergrad.yml happy
73fcec28
got rid of classical in definition of single
e3b8a011
decidability fixes
ff554032
add decidability reqs in spectrum
f0204507
fix decidability conditions in sphere
b513e1c6
fewer decidable
14eac753
lint
99d94d15
omit one more
0c58bb48
Begin
51f2c824
++
c6790492
Basic definitions
30245438
Start key lemma
aab13b00
One annoying sorry down
0aacd852
++
25fe4d10
Small progress
34d4c9b5
++
80d1314c
moved lemma and golfed proof
6d8c18c9
Progress
e1471bd0
golfd coe_of_repr, removed coe_reindex_repr
4ab33569
Merge remote-tracking branch 'origin/master' into std_orthonormal_basis
9ca4c80e
fixed proof of linear_independent.finite
b2ad495e
removed module from module_is_internal
f795d60b
fixed sphere.lean
d20266e1
fixed spectrum.lean
9bbb0447
fixed matrix spectral_theorem
abe0dfaf
Fixed docstring comments
cda9fa89
Merge remote-tracking branch 'origin/master' into std_orthonormal_basis
d95493ae
Add auxiliary defs everywhere; need cache
59d802a3
Yay !
904be9d3
Remove two easy sorries
1f22f00e
Need merge
b7c618f1
Merge remote-tracking branch 'origin/std_orthonormal_basis' into AD_t…
9a0a32d4
orientation.fin_orthonormal_basis now an onb
12ee2143
Sorry free (finally...)
dcdac9b1
Revert "orientation.fin_orthonormal_basis now an onb"
4924e8ff
Merge remote-tracking branch 'origin/std_orthonormal_basis' into AD_t…
9090771a
Define positive operators
a27ba1b4
Merge branch 'AD_positive_operator' into AD_trace_class_3
95a236cf
Long line
258cff68
Long line 2
3c5e1a0d
Merge remote-tracking branch 'origin/master' into AD_trace_class_3
f2965a6e
`linear_equiv.of_eq` as a `linear_isometry_equiv`
90722c0e
Unused argument
774e2447
Merge branch 'AD_linear_isometry_equiv_of_eq' into AD_trace_class_3
affbd1df
A finite orthonormal family is an orthonormal
6c61ebb7
Merge branch 'AD_orthonormal_basis_span' into AD_trace_class_3
94a94ba3
Fix
f5e69f5c
Apply suggestions from code review
f7d21b21
Factor
d9e16271
Use cod_restrict
25f54cbd
WIP
de2f57ef
Rename
9fe498b2
Merge remote-tracking branch 'origin/master' into AD_trace_class_3
6c15a884
Compute inner product in a given basis
5fd0e1d8
Merge branch 'AD_orthonormal_basis_span' into AD_trace_class_3
a8ea5c15
Merge branch 'AD_sum_inner_mul_inner' into AD_trace_class_3
f2f1cb54
Smarter proof
eb27e9cb
Merge remote-tracking branch 'origin/AD_positive_operator' into AD_tr…
751056fe
Merge remote-tracking branch 'origin/AD_linear_isometry_equiv_of_eq' …
09f4ce80
Merge remote-tracking branch 'origin/AD_sum_inner_mul_inner' into AD_…
4b0c7145
In finite dimension, hilbert = orthonormal
0f411220
Merge branch 'AD_hilbert_orthonormal' into AD_trace_class_3
1ef062f1
Add coe lemma
7d70b14b
Init
3f5d12a2
Merge remote-tracking branch 'origin/AD_hilbert_orthonormal' into AD_…
a5baeee3
++
5781b207
Merge branch 'AD_orthonormal_basis_span' into AD_proj_basis
279c306f
Merge branch 'AD_proj_basis' into AD_trace_class_3
7c72e40c
Move
5b715bbc
Suggestions
bec5ee2d
Fix
05391713
Merge remote-tracking branch 'origin/AD_linear_isometry_equiv_of_eq' …
3730aea3
Merge remote-tracking branch 'origin/AD_orthonormal_basis_span' into …
f08666da
Merge remote-tracking branch 'origin/AD_proj_basis' into AD_trace_cla…
96bfeb9b
Fixes
d4001fe7
`tsum` version
20504ee1
Merge branch 'AD_sum_inner_mul_inner' into AD_trace_class_3
3bcc725f
FIx
d61be92b
Merge branch 'AD_orthonormal_basis_span' into AD_proj_basis
d19fce30
No @[simps]
cba6d459
Merge branch 'AD_linear_isometry_equiv_of_eq' into AD_orthonormal_bas…
40b81e35
Merge remote-tracking branch 'origin/master' into AD_hilbert_orthonormal
1fafcb24
Merge branch 'AD_hilbert_orthonormal' into AD_proj_basis
2c9b82ed
Merge remote-tracking branch 'origin/master' into AD_trace_class_3
dfbd84fd
Fix
d83cf9d5
Bit of cleanup
39056cea
`orthonormal` version of `linear_independent.coe_range`
0c5f6a34
Variant of `continuous_linear_equiv.has_sum`
b02b2c3d
Merge branch 'AD_continuous_linear_equiv_sum' into AD_trace_class_3
6a5e3a29
Merge branch 'AD_orthonormal_coe_range' into AD_trace_class_3
a401db64
Fix again
8c42281d
Docstrings
1575d250
Merge branch 'AD_hilbert_orthonormal' into AD_proj_basis
e6b482ea
Merge remote-tracking branch 'origin/master' into AD_trace_class_3
c7ca450d
Merge remote-tracking branch 'origin/master' into AD_proj_basis
00253ea2
Merge branch 'AD_orthonormal_basis_span' into AD_trace_class_3
70cc29ee
Dependent type hell
2fd5e111
Fix
0799ae10
++
100196fa
Jireh's suggestions
100268d8
Merge remote-tracking branch 'origin/master' into AD_proj_basis
099099d3
I should think
14169dc7
Success !
c5bcbff8
Clean
80f9026d
Main thm !
24f5ad1c
Small progress
9b95fdf9
Merge remote-tracking branch 'origin/master' into AD_orthonormal_basi…
9376459c
Merge remote-tracking branch 'origin/master' into AD_hilbert_orthonormal
865f1f67
Merge branch 'AD_hilbert_orthonormal' into AD_proj_basis
6f92b5a6
Merge branch 'AD_orthonormal_basis_span' into AD_proj_basis
2d4c8353
Merge branch 'AD_proj_basis' into AD_trace_class_3
8ded5e56
Remove useless `complete_space E` assumption
162d95db
Useless argument later
51b3f757
Merge remote-tracking branch 'origin/AD_less_completeness' into AD_pr…
b5dae8f1
Heather's suggestions
1ff6a440
++
f187be2f
Duplicate argument
a5316473
DTT hell strikes again
9dca747e
Merge remote-tracking branch 'origin/master' into AD_proj_basis
8b14198b
Induction is incredible
e7a0d977
Super annoying timeout
3bd3af67
Timeout fixed :tada:
4e73262c
Merge remote-tracking branch 'origin/master' into AD_proj_basis
3e3c6fbe
Indentation
10231e42
Done ?
66df8034
Merge branch 'AD_subordinate_hilbert_basis' into AD_trace_class_3
8b68ee17
Merge remote-tracking branch 'origin/master' into AD_trace_class_3
e46ee8b9
Start
e7938ed6
...
89a9ab9e
Useless
28290053
Basics
2db919b2
Congr right
266ab572
Fixes
738aed0c
++
53e99595
Use `expand_exists`
d75d48ff
Name clash
8fab2bd5
Make `function.injective.decidable_eq` protected
9af03251
Merge branch 'AD_injective_decidable_eq_protected' into AD_lp_functorial
c7f9f618
Define`is_hilbert_sum` predicate
691c6557
Update src/analysis/normed_space/lp_space.lean
4c25aeb0
Finish renaming
9ff6e5a4
Semilinearize
4f4f6209
Lint
30df7ef0
Merge branch 'AD_lp_functorial' into AD_lp_curry
f9e84f27
Done
11bbcb9d
Merge branch 'AD_lp_curry' into AD_subordinate_hilbert_basis
e4be6302
Merge remote-tracking branch 'origin/AD_is_hilbert_sum' into AD_subor…
875443fd
Collect Hilbert bases along a Hilbert sum decomposition
21ef33c8
Long line
19c3fab9
Protect proj
e971af78
Merge branch 'AD_subordinate_hilbert_basis' into AD_trace_class_3
c910a98e
Done !
daa15566
Unused arguments
3ad9537f
Merge branch 'AD_subordinate_hilbert_basis' into AD_trace_class_3
c6437d15
Merge branch 'AD_orthogonal_hilbert_sum' into AD_trace_class_3
5b5a2af6
Lint
e12d3a60
YES !
6d3977ef
tmp
91ec0986
Various facts about `orthogonal_projection`
7c690c06
Empty case
59ab4dea
Merge branch 'AD_orthogonal_projection_facts' into AD_trace_class_3
c14b36a3
Merge branch 'AD_orthogonal_projection_facts' into AD_proj_basis
cd1d659c
Fix
073e2a80
Use general version
00eccd45
Avoid bases, deep cleanup
97cd3bfb
Define `hilbert_basis.partial_span`
3863707a
Merge branch 'AD_hilbert_basis_partial_spans' into AD_proj_basis
5456e36a
Use `partial_span`
b926a532
Merge branch 'AD_proj_basis' into AD_trace_class_3
37233d1b
Remove sorry
2ba359ff
Nice progress
ea16f9cf
Partial reverse to bases :/
7c4aeb75
Reviewers
No reviews
Assignees
No one assigned
Labels
WIP
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub