OAI/MathematicalPhysics/Boltzmann/Branching/ComplexWeakL2Diagonal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Weak subsequences in the complex L2 space used by the Fourier proof

  1. theorem OAI.BoltzmannNonuniqueness.Published.exists_weak_complex_L2_subsequence line 18
  2. theorem OAI.BoltzmannNonuniqueness.Published.complex_weak_norm_le line 55
  3. def OAI.BoltzmannNonuniqueness.Published.complexL2Restriction line 80
  4. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Restriction_ae line 84
  5. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Restriction_sub line 88
  6. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Restriction_norm_le line 99
  7. theorem OAI.BoltzmannNonuniqueness.Published.complexL2Restriction_norm_sq line 105
  8. theorem OAI.BoltzmannNonuniqueness.Published.exists_common_weak_complex_L2_subsequence line 130