Basic.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.EntropyPhotonNumber.NumberIndex line 12
Source documentation
The number-basis indices for n bosonic modes.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:12 (same declaration text).
```
abbrev NumberIndex (n : ℕ) := Fin n → ℕ
```
abbrev OAI.EntropyPhotonNumber.Fock line 15
Source documentation
The full, untruncated bosonic Fock space ℓ²(ℕⁿ, ℂ).
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:15 (same declaration text).
```
abbrev Fock (n : ℕ) := lp (fun _ : NumberIndex n => ℂ) 2
```
Mentions: OAI.EntropyPhotonNumber.NumberIndex
def OAI.EntropyPhotonNumber.numberKet line 18
Source documentation
A number-basis vector.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:18 (same declaration text).
```
def numberKet {n : ℕ} (k : NumberIndex n) : Fock n := lp.single 2 k 1
```
Mentions: OAI.EntropyPhotonNumber.NumberIndex, OAI.EntropyPhotonNumber.Fock
def OAI.EntropyPhotonNumber.entry line 21
Source documentation
Matrix entries of an operator in the number basis.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:21 (same declaration text).
```
def entry {n : ℕ} (T : Fock n →L[ℂ] Fock n) (k l : NumberIndex n) : ℂ :=
…
```
Mentions: OAI.EntropyPhotonNumber.Fock, OAI.EntropyPhotonNumber.NumberIndex
structure OAI.EntropyPhotonNumber.State line 27
Source documentation
Positive trace-one operators. For a positive bounded operator on this Hilbert space, summability of its diagonal is the positive trace-class criterion; HasSum ... 1 includes summability as well as normalization.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:27 (same declaration text).
```
structure State (n : ℕ) where
…
```
def OAI.EntropyPhotonNumber.totalNumber line 33
Source documentation
Total number of quanta in a number-basis vector.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:33 (same declaration text).
```
def totalNumber {n : ℕ} (k : NumberIndex n) : ℕ := ∑ j, k j
```
Mentions: OAI.EntropyPhotonNumber.NumberIndex
def OAI.EntropyPhotonNumber.FiniteEnergy line 36
Source documentation
Exactly finiteness of the expectation of the nonnegative number operator.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:36 (same declaration text).
```
def FiniteEnergy {n : ℕ} (ρ : State n) : Prop :=
…
```
Mentions: OAI.EntropyPhotonNumber.State
def OAI.EntropyPhotonNumber.entropy line 41
Source documentation
−Tr ρ log ρ, using the continuous extension of −t log t at zero and continuous functional calculus for the positive operator ρ.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:41 (same declaration text).
```
def entropy {n : ℕ} (ρ : State n) : ℝ :=
…
```
Mentions: OAI.EntropyPhotonNumber.State
def OAI.EntropyPhotonNumber.g line 46
Source documentation
The thermal entropy per mode; Lean's Real.log 0 = 0 implements exactly the stated convention 0 log 0 = 0.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:45 (same declaration text).
```
def g (t : ℝ) : ℝ := (t + 1) * Real.log (t + 1) - t * Real.log t
```
def OAI.EntropyPhotonNumber.gInv line 50
Source documentation
The inverse of increasing g : [0,∞) → [0,∞), expressed by its lower level cut. Only its values on [0,∞) occur in the main theorem.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:49 (same declaration text).
```
def gInv (s : ℝ) : ℝ := sInf {t : ℝ | 0 ≤ t ∧ s ≤ g t}
```
Mentions: OAI.EntropyPhotonNumber.g
def OAI.EntropyPhotonNumber.oneModeBeamCoefficient line 56
Source documentation
One-mode passive beam-splitter coefficient, in number bases. It is the coefficient of (c†)^k (d†)^e in (√η c† − √(1−η) d†)^a (√(1−η) c† + √η d†)^b, with the normalized number-vector factorials.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:55 (same declaration text).
```
def oneModeBeamCoefficient (η : ℝ) (k e a b : ℕ) : ℝ :=
…
```
Mentions: OAI.EntropyPhotonNumber.b
def OAI.EntropyPhotonNumber.beamCoefficient line 68
Source documentation
The same passive rotation is performed on all mode indices.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:67 (same declaration text).
```
def beamCoefficient {n : ℕ} (η : ℝ) (k e a b : NumberIndex n) : ℝ :=
…
```
Mentions: OAI.EntropyPhotonNumber.b, OAI.EntropyPhotonNumber.NumberIndex
abbrev OAI.EntropyPhotonNumber.SectorSplit line 72
Source documentation
Choices of the first input number in the total-number sector of (k,e).
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:71 (same declaration text).
```
abbrev SectorSplit {n : ℕ} (k e : NumberIndex n) := ∀ j, Fin (k j + e j + 1)
```
Mentions: OAI.EntropyPhotonNumber.NumberIndex
def OAI.EntropyPhotonNumber.splitLeft line 74
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:73 (same declaration text).
def OAI.EntropyPhotonNumber.splitRight line 77
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:76 (same declaration text).
def OAI.EntropyPhotonNumber.outputBlock line 83
Source documentation
A single discarded-number diagonal block of U(ρA ⊗ ρB)U†. The sums are finite because passive mixing preserves number in each paired mode. The two unrestricted density matrices allow all internal entanglement.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:82 (same declaration text).
```
def outputBlock {n : ℕ} (η : ℝ) (ρA ρB : State n)
    (k l e : NumberIndex n) : ℂ :=
…
```
Mentions: OAI.EntropyPhotonNumber.State, OAI.EntropyPhotonNumber.NumberIndex
def OAI.EntropyPhotonNumber.IsBeamSplitterOutput line 95
Source documentation
Reduced state after passive beam-splitter mixing of independent ports. The second row of the orthogonal rotation is (-√(1−η),√η); changing its sign has no effect on this reduced state. HasSum records the actual partial trace, not a default value for a possibly divergent series.
Also declared: ComparatorChallenges/EntropyPhotonNumber.lean:94 (same declaration text).
```
def IsBeamSplitterOutput {n : ℕ} (η : ℝ) (ρA ρB ρC : State n) : Prop :=
…
```
Mentions: OAI.EntropyPhotonNumber.State