ImmFirstMomentBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.immFirstMomentMean line 12
Source documentation
The independent geometric benchmark for one IMM path.
```
def immFirstMomentMean (n : ℕ) (side : Fin n → Bool) (a b : ℕ) : ℝ :=
…
```
def OAI.Problem335.immFirstMomentLoss line 19
Source documentation
The explicit finite-size occupation loss, before parameter specialization.
```
def immFirstMomentLoss (n : ℕ) (side : Fin n → Bool) (a b : ℕ) : ℝ :=
…
```

theorem OAI.Problem335.immNormalizedMatrix_first_moment_lower line 30

Source documentation

First-moment lower bound for the actual finite normalized IMM matrix. The only hypotheses are positive occupation totals, nonempty variable groups, and the elementary order range required by the occupation ratio estimate.

theorem immNormalizedMatrix_first_moment_lower
    (n : ℕ) (hn : 0 < n) (side : Fin n → Bool) (a b : ℕ)
    [Nonempty {x : Fin n × Fin n × Fin n // side x.1 = true}]
    [Nonempty {x : Fin n × Fin n × Fin n // side x.1 = false}]
    (ha : 0 < a) (hb : 0 < b)
    (hk : 2 * immLayerVCount side ≤ a) (hm : 2 * immLayerUCount side ≤ b) :
    (Fintype.card (ImmSourceIndex n side a b) : ℝ) * (n : ℝ) ^ (n - 1) *
        (Real.exp (-immFirstMomentLoss n side a b) * immFirstMomentMean n side a b) ≤
      ((immNormalizedMatrix n side a b).conjTranspose *
        immNormalizedMatrix n side a b).trace.re := by
…

Mentions: OAI.Problem335.immLayerVCount, OAI.Problem335.immLayerUCount, OAI.Problem335.ImmSourceIndex, OAI.Problem335.immFirstMomentLoss, OAI.Problem335.immFirstMomentMean, OAI.Problem335.immNormalizedMatrix