OAI/Analysis/FreeEntropy/TwoNoiseFisher.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.fisher_le_scaled_test line 12
  2. theorem OAI.FiniteEntropySeparation.norm_sq_sqrt_pair line 30
  3. theorem OAI.FiniteEntropySeparation.FreeTensor.noise_basis_test line 42
  4. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_vacuum line 55
  5. theorem OAI.FiniteEntropySeparation.Model.initialIndex_fresh line 64
  6. def OAI.FiniteEntropySeparation.Model.doublyNoised line 68
  7. def OAI.FiniteEntropySeparation.Model.noiseVector₀ line 69
  8. def OAI.FiniteEntropySeparation.Model.noiseVector₁ line 70
  9. theorem OAI.FiniteEntropySeparation.Model.doublyNoised_comm line 72
  10. theorem OAI.FiniteEntropySeparation.Model.auxiliaryBackground_mem line 78
  11. theorem OAI.FiniteEntropySeparation.Model.noiseVector₀_test line 84
  12. theorem OAI.FiniteEntropySeparation.Model.noiseVector₁_test line 91
  13. theorem OAI.FiniteEntropySeparation.Model.noiseVector₀_norm line 98
  14. theorem OAI.FiniteEntropySeparation.Model.noiseVector₁_norm line 102
  15. theorem OAI.FiniteEntropySeparation.Model.noiseVector_orthogonal line 104
  16. theorem OAI.FiniteEntropySeparation.Model.doublyNoised_fisher_le line 111
  17. theorem OAI.FiniteEntropySeparation.Model.noiseVector₀_C line 126
  18. theorem OAI.FiniteEntropySeparation.Model.noiseVector₁_C line 130
  19. theorem OAI.FiniteEntropySeparation.Model.doublyNoised_vacuum line 135
  20. theorem OAI.FiniteEntropySeparation.Model.doublyNoised_variance line 144
  21. theorem OAI.FiniteEntropySeparation.Model.C_vacuum_norm_sq_le line 157
  22. theorem OAI.FiniteEntropySeparation.Model.doublyNoised_fisher_lower line 164