OAI/Analysis/TriangularHilbert/DissipationAlgebra.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.TriangularHilbert.Heat.finite_cost_dissipationline 10 - lemma
OAI.TriangularHilbert.Heat.offdiag_sum_eqline 49 - lemma
OAI.TriangularHilbert.Heat.neighbor_one_neline 53 - lemma
OAI.TriangularHilbert.Heat.neighbor_two_neline 54 - lemma
OAI.TriangularHilbert.Heat.neighbors_neline 55