OAI/Analysis/LiebThirring/SpectralTrials.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.SpectralProof.triangular_action_upper line 14
2. lemma OAI.SharpLiebThirring.SpectralProof.finite_spectral_trial line 56
3. lemma OAI.SharpLiebThirring.SpectralProof.compact_family_radius line 86
4. lemma OAI.SharpLiebThirring.SpectralProof.integral_eq_interval_of_vanish line 102
5. lemma OAI.SharpLiebThirring.SpectralProof.row_mem_prefix line 110
6. lemma OAI.SharpLiebThirring.SpectralProof.compact_trial_energy line 120
7. lemma OAI.SharpLiebThirring.SpectralProof.compact_trial_bound line 143