UniformIndexCoupling.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.root_uniform_bound line 14
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_root line 25
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_root_base line 35

theorem OAI.DilutedSpinGlass.FiniteLaw.Projects.pi line 57

Source documentation

Coordinatewise pushforwards tensorize even for tests that do not factor.

theorem Projects.pi {ι : Type*} [Fintype ι] [DecidableEq ι]
    {α β : ι → Type*} [∀ i, Fintype (α i)] [∀ i, Fintype (β i)]
    {P : (i : ι) → FiniteLaw (α i)} {Q : (i : ι) → FiniteLaw (β i)}
    {π : (i : ι) → α i → β i} (h : ∀ i, Projects (P i) (Q i) (π i)) :
    Projects (FiniteLaw.pi P) (FiniteLaw.pi Q) (fun x i => π i (x i)) := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.Projects, OAI.DilutedSpinGlass.FiniteLaw.pi

def OAI.DilutedSpinGlass.SizeCoupling.indexLaw line 74
Source documentation
Choose a potential new index uniformly and an independent old fallback. Only the zero new index uses the fallback; all other old indices coincide.
```
noncomputable def indexLaw (N : ℕ) [NeZero N] : FiniteLaw (Fin (N+1) × Fin N) :=
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw
def OAI.DilutedSpinGlass.SizeCoupling.oldIndex line 77
def OAI.DilutedSpinGlass.SizeCoupling.newIndex line 79
theorem OAI.DilutedSpinGlass.SizeCoupling.oldIndex_projects line 81
theorem OAI.DilutedSpinGlass.SizeCoupling.newIndex_projects line 95
theorem OAI.DilutedSpinGlass.SizeCoupling.newIndex_probability line 101
Source documentation
The exact probability of changing a site is 1/(N+1).
```
theorem newIndex_probability (N : ℕ) [NeZero N] :
    (indexLaw N).expect (fun z => if z.1 = 0 then (1:ℝ) else 0) = 1/(N+1) := by
…
```
Mentions: OAI.DilutedSpinGlass.SizeCoupling.indexLaw
lemma OAI.DilutedSpinGlass.SizeCoupling.same_index_off_new line 109
theorem OAI.DilutedSpinGlass.SizeCoupling.expected_new_count line 116