OAI/Analysis/HardSphere/Density/GroundProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.groundSpace_finiteDimensional line 15
2. lemma OAI.HardSphere.groundSupported_iff_support_le line 30
3. lemma OAI.HardSphere.groundSpace_nontrivial_of_ne_bot line 56
4. abbrev OAI.HardSphere.normalizedGroundProjection line 69

   Source documentation

   Precisely Π/Tr Π for the orthogonal projection on the entire bosonic ground space. The nonzero condition is exactly the domain of normalization, not a finite-rank assumption.

   abbrev normalizedGroundProjection (N : ℕ) (L : Length) (a : ℝ)
       (ha : @LT.lt ℝ Real.instLT (@Zero.zero ℝ Real.instZero) a)
       (hG : @Ne (@Submodule ℂ (ScalarL2 N L) Complex.instSemiring
         (scalarL2_normedAddCommGroup N L).toAddCommMonoid (scalarL2_module N L))
         (groundSpace N L a) (@Bot.bot
           (@Submodule ℂ (ScalarL2 N L) Complex.instSemiring
             (scalarL2_normedAddCommGroup N L).toAddCommMonoid (scalarL2_module N L))
           (@Submodule.instBot ℂ (ScalarL2 N L) Complex.instSemiring
           (scalarL2_normedAddCommGroup N L).toAddCommMonoid (scalarL2_module N L)))) :
       @Density.Operator (ScalarL2 N L) (scalarL2_normedAddCommGroup N L)
         (scalarL2_innerProductSpace N L) (scalarL2_completeSpace N L) :=
   …

   Mentions: OAI.HardSphere.Length, OAI.HardSphere.ScalarL2, OAI.HardSphere.scalarL2_normedAddCommGroup, OAI.HardSphere.scalarL2_module, OAI.HardSphere.groundSpace, OAI.HardSphere.Density.Operator, OAI.HardSphere.scalarL2_innerProductSpace, OAI.HardSphere.scalarL2_completeSpace

5. lemma OAI.HardSphere.normalizedGroundProjection_formula line 86
6. lemma OAI.HardSphere.normalizedGroundProjection_supported line 93
7. lemma OAI.HardSphere.IsGroundVector.groundSpace_ne_bot line 102