OAI/Probability/DilutedSpin/DepthChildMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.DepthAverage.average_nonneg line 14
2. lemma OAI.DilutedSpinGlass.DepthAverage.average_mono line 22
3. lemma OAI.DilutedSpinGlass.DepthAverage.average_const_mul line 30
4. lemma OAI.DilutedSpinGlass.DepthAverage.average_sqrt_le line 38
5. lemma OAI.DilutedSpinGlass.DepthAverage.fiber_sqrt_bound line 49
6. theorem OAI.DilutedSpinGlass.DepthAverage.fiber_child_moment_bound line 61

   Source documentation

   The exact nested square roots occurring in the physical root multileaf estimate pass through the normalized depth fibers. Every child uses its own retained coordinates; unused coordinates have mass one.

   theorem fiber_child_moment_bound {ι : Type} [Fintype ι]
       {β : ι → Type} [∀ j, Fintype (β j)] [∀ j, DecidableEq (β j)]
       (c : ℝ) (hc : 0≤c) (e : (j : ι) → β j → α) (he : ∀ j, Function.Injective (e j))
       (τ : (j : ι) → β j → Equiv.Perm (Fin L))
       (D : (α → Fin L) → Prop) (E : (j : ι) → (β j → Fin L) → Prop)
       (hDE : ∀ j q, D q → E j (coordinateProjection (e j) (τ j) q))
       (F : (j : ι) → (β j → Fin L) → ℝ) (hF : ∀ j q, 0≤F j q) :
       average D (fun q => Real.sqrt (c*∑ j, Real.sqrt (F j (coordinateProjection (e j) (τ j) q)))) ≤
         Real.sqrt (c*∑ j, Real.sqrt (average (E j) (F j))) := by
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.DepthAverage.coordinateProjection, OAI.DilutedSpinGlass.DepthAverage.average