OAI/Probability/EntangledGames/SpectralEntropy.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThresholdParallelRepetition.Resolvent.isClosed_posSemidef line 26
  2. lemma OAI.ThresholdParallelRepetition.Resolvent.integral_matrix_nonneg line 44
  3. lemma OAI.ThresholdParallelRepetition.Resolvent.integral_matrix_mono line 51
  4. def OAI.ThresholdParallelRepetition.Resolvent.spectralLinear line 56
  5. lemma OAI.ThresholdParallelRepetition.Resolvent.spectralLinear_apply line 76
  6. lemma OAI.ThresholdParallelRepetition.Resolvent.cfc_eq_spectralLinear line 79
  7. lemma OAI.ThresholdParallelRepetition.Resolvent.integrable_cfc line 85
  8. lemma OAI.ThresholdParallelRepetition.Resolvent.integral_cfc line 92
  9. lemma OAI.ThresholdParallelRepetition.Resolvent.spectrum_nonneg line 111
  10. lemma OAI.ThresholdParallelRepetition.Resolvent.eigenvalues_le_one line 117
  11. lemma OAI.ThresholdParallelRepetition.Resolvent.resolvent_cfc line 126
  12. lemma OAI.ThresholdParallelRepetition.Resolvent.purificationKernel_cfc line 137
  13. lemma OAI.ThresholdParallelRepetition.Resolvent.purificationKernel_square_cfc line 150
  14. lemma OAI.ThresholdParallelRepetition.Resolvent.kernel_square_integrable line 163
  15. lemma OAI.ThresholdParallelRepetition.Resolvent.kernel_square_integral line 172
  16. def OAI.ThresholdParallelRepetition.Resolvent.effectEntropy line 187
  17. def OAI.ThresholdParallelRepetition.Resolvent.entropyIntegrand line 189
  18. lemma OAI.ThresholdParallelRepetition.Resolvent.entropyIntegrand_cfc line 192
  19. lemma OAI.ThresholdParallelRepetition.Resolvent.entropy_integrable line 205
  20. lemma OAI.ThresholdParallelRepetition.Resolvent.entropy_integral line 214
  21. lemma OAI.ThresholdParallelRepetition.Resolvent.scalar_kernel_memLp line 243
  22. lemma OAI.ThresholdParallelRepetition.Resolvent.kernel_entry_memLp line 249
  23. lemma OAI.ThresholdParallelRepetition.Resolvent.integrable_gram line 266
  24. lemma OAI.ThresholdParallelRepetition.Resolvent.kernel_cross_integrable line 281
  25. lemma OAI.ThresholdParallelRepetition.Resolvent.kernel_distance_integrable line 285
  26. lemma OAI.ThresholdParallelRepetition.Resolvent.entropy_gap_integrand_eq line 301
  27. lemma OAI.ThresholdParallelRepetition.Resolvent.weighted_distance_jensen line 321