FirstOccupationMoment.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.occupationAverage line 12
Source documentation
Uniform average over all weak compositions of t in the coordinates ι.
```
def occupationAverage {ι : Type*} [Fintype ι] [DecidableEq ι]
    (t : ℕ) (f : (ι →₀ ℕ) → ℝ) : ℝ :=
…
```
lemma OAI.Problem335.occupationAverage_sum line 17
lemma OAI.Problem335.occupationAverage_nonneg line 24

theorem OAI.Problem335.occupationAverage_prod line 31

Source documentation

The squarefree occupation product needed by differentiated path layers.

theorem occupationAverage_prod {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι]
    (t : ℕ) (s : Finset ι) :
    occupationAverage t (fun M => ∏ i ∈ s, (M i : ℝ)) =
      (t.descFactorial s.card : ℝ) / ((Fintype.card ι).ascFactorial s.card : ℝ) := by
…

Mentions: OAI.Problem335.occupationAverage

theorem OAI.Problem335.occupationAverage_prod_add_one line 39

Source documentation

Multiplication layers supply successor occupations; expand them by subsets.

theorem occupationAverage_prod_add_one {ι : Type*} [Fintype ι] [DecidableEq ι]
    [Nonempty ι] (t : ℕ) (s : Finset ι) :
    occupationAverage t (fun M => ∏ i ∈ s, ((M i : ℝ) + 1)) =
      ∑ z ∈ s.powerset,
        (t.descFactorial z.card : ℝ) / ((Fintype.card ι).ascFactorial z.card : ℝ) := by
…

Mentions: OAI.Problem335.occupationAverage

lemma OAI.Problem335.occupation_powerset_sum line 48

theorem OAI.Problem335.occupationAverage_prod_add_one_lower_of_factorial line 53

Source documentation

A uniform factorial-moment loss transfers to the successor product.

theorem occupationAverage_prod_add_one_lower_of_factorial {ι : Type*}
    [Fintype ι] [DecidableEq ι] [Nonempty ι] (t : ℕ) (s : Finset ι) (L : ℝ)
    (hL : ∀ H ≤ s.card,
      L * ((t : ℝ) / Fintype.card ι) ^ H ≤
        (t.descFactorial H : ℝ) / ((Fintype.card ι).ascFactorial H : ℝ)) :
    L * (1 + (t : ℝ) / Fintype.card ι) ^ s.card ≤
      occupationAverage t (fun M => ∏ i ∈ s, ((M i : ℝ) + 1)) := by
…

Mentions: OAI.Problem335.occupationAverage

theorem OAI.Problem335.occupationAverage_tensor line 68

Source documentation

Independent composition averages factor without any probabilistic independence convention being implicit.

theorem occupationAverage_tensor {ι κ : Type*} [Fintype ι] [DecidableEq ι]
    [Fintype κ] [DecidableEq κ] (a b : ℕ)
    (f : (ι →₀ ℕ) → ℝ) (g : (κ →₀ ℕ) → ℝ) :
    (∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset ι) a,
      ∑ N ∈ Finset.finsuppAntidiag (Finset.univ : Finset κ) b, f M * g N) /
        ((Finset.finsuppAntidiag (Finset.univ : Finset ι) a).card *
          (Finset.finsuppAntidiag (Finset.univ : Finset κ) b).card : ℝ) =
      occupationAverage a f * occupationAverage b g := by
…

Mentions: OAI.Problem335.occupationAverage

theorem OAI.Problem335.occupationAverage_prod_le line 79
theorem OAI.Problem335.occupationAverage_prod_lower line 86
theorem OAI.Problem335.occupationAverage_prod_add_one_le line 94
theorem OAI.Problem335.occupationAverage_prod_add_one_lower line 103

theorem OAI.Problem335.occupation_first_moment_lower line 114

Source documentation

The two-group first-trace occupation estimate, with its exact finite-size loss and no asymptotic or independence premises.

theorem occupation_first_moment_lower {V U : Type*}
    [Fintype V] [DecidableEq V] [Nonempty V]
    [Fintype U] [DecidableEq U] [Nonempty U]
    (a b : ℕ) (s : Finset V) (z : Finset U)
    (ha : 0 < a) (hb : 0 < b) (hs : 2 * s.card ≤ a) (hz : 2 * z.card ≤ b) :
    Real.exp ((-(s.card : ℝ) ^ 2 / a - (s.card : ℝ) ^ 2 / (2 * Fintype.card V)) +
        (-(z.card : ℝ) ^ 2 / b - (z.card : ℝ) ^ 2 / (2 * Fintype.card U))) *
      (((a : ℝ) / Fintype.card V) ^ s.card *
        (1 + (b : ℝ) / Fintype.card U) ^ z.card) ≤
      (∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset V) a,
        ∑ N ∈ Finset.finsuppAntidiag (Finset.univ : Finset U) b,
          (∏ i ∈ s, (M i : ℝ)) * (∏ j ∈ z, ((N j : ℝ) + 1))) /
…