OAI/Probability/DilutedSpin/SpinRootData.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PhysicalRoot.energy line 16

   Source documentation

   Literal physical spin weight, with the independent physical root inputs kept as a recursive product only for the variance calculation.

   noncomputable def energy (V : X → (Fin N → Spin) → ℝ) (field : Y → ℝ)
       (h : RootPath Y N) (k : ℕ) (x : RootPath X k) (σ : Fin N → Spin) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.RootPath

2. def OAI.DilutedSpinGlass.PhysicalRoot.interactionValue line 21

   Source documentation

   The interaction label includes the p uniform indices, with repetitions.

   noncomputable def interactionValue {p : ℕ}
       (z : InteractionSample p × (Fin p → Fin N)) (σ : Fin N → Spin) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin

3. theorem OAI.DilutedSpinGlass.PhysicalRoot.energy_eq_logWeight line 25
4. theorem OAI.DilutedSpinGlass.PhysicalRoot.measurable_interactionValue line 31
5. theorem OAI.DilutedSpinGlass.PhysicalRoot.interactionValue_bound line 37
6. theorem OAI.DilutedSpinGlass.PhysicalRoot.sum_update_difference line 41
7. theorem OAI.DilutedSpinGlass.PhysicalRoot.measurable_energy line 51
8. theorem OAI.DilutedSpinGlass.PhysicalRoot.abs_spin line 60
9. theorem OAI.DilutedSpinGlass.PhysicalRoot.energy_bound line 64
10. theorem OAI.DilutedSpinGlass.PhysicalRoot.energy_replace_interaction line 81
11. theorem OAI.DilutedSpinGlass.PhysicalRoot.energy_add_interaction line 90
12. theorem OAI.DilutedSpinGlass.PhysicalRoot.energy_replace_field line 98
13. lemma OAI.DilutedSpinGlass.FiniteLaw.uniform_equiv line 118
14. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_fourthRoot_le line 124
15. def OAI.DilutedSpinGlass.DepthAverage.depthLaw line 138
16. def OAI.DilutedSpinGlass.DepthAverage.average line 141
17. lemma OAI.DilutedSpinGlass.DepthAverage.average_eq line 144
18. def OAI.DilutedSpinGlass.DepthAverage.coordinateProjection line 152
19. lemma OAI.DilutedSpinGlass.DepthAverage.depthLaw_projection line 155
20. theorem OAI.DilutedSpinGlass.DepthAverage.fiber_bound line 170

    Source documentation

    Exact fiber comparison with normalized unused coordinates. The retained coordinates may independently be shifted by any permutation.

    theorem fiber_bound (e : β → α) (he : Function.Injective e)
        (τ : β → Equiv.Perm (Fin L)) (D : (α → Fin L) → Prop) (E : (β → Fin L) → Prop)
        (hDE : ∀ q, D q → E (coordinateProjection e τ q)) (F : (β → Fin L) → ℝ)
        (hF : ∀ q, 0 ≤ F q) : average D (fun q => F (coordinateProjection e τ q)) ≤ average E F := by
    …

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

21. theorem OAI.DilutedSpinGlass.DepthAverage.fiber_fourthRoot_bound line 189

    Source documentation

    The fourth-root form of decor:fiber-bound, with no diagonal restriction of independently sampled aligned copies and no volume-ratio loss.

    theorem fiber_fourthRoot_bound (e : β → α) (he : Function.Injective e)
        (τ : β → Equiv.Perm (Fin L)) (D : (α → Fin L) → Prop) (E : (β → Fin L) → Prop)
        (hDE : ∀ q, D q → E (coordinateProjection e τ q)) (F : (β → Fin L) → ℝ)
        (hF : ∀ q, 0 ≤ F q) :
        average D (fun q => Real.sqrt (Real.sqrt (F (coordinateProjection e τ q)))) ≤
          Real.sqrt (Real.sqrt (average E F)) := by
    …

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