OAI/Probability/DilutedSpin/ReservoirVariance.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.measurableEmbedding_sigmaMk line 13
2. theorem OAI.DilutedSpinGlass.measurable_sigmaProd line 37

   Source documentation

   Countable disjoint root laws retain joint parameter measurability.

   theorem measurable_sigmaProd {I : Type*} [Countable I] {X : I → Type*}
       [∀ i, MeasurableSpace (X i)] {A Y : Type*} [MeasurableSpace A] [MeasurableSpace Y]
       {f : (i : I) → X i → A → Y}
       (hf : ∀ i, Measurable (fun z : X i × A => f i z.1 z.2)) :
       Measurable (fun z : Sigma X × A => f z.1.1 z.1.2 z.2) := by
   …

3. theorem OAI.DilutedSpinGlass.KernelTower.measurable_correctedPerturbLog line 67
4. theorem OAI.DilutedSpinGlass.KernelTower.measurable_correctedPerturbScore line 76
5. theorem OAI.DilutedSpinGlass.KernelTower.correctedPerturbScore_bound line 87
6. theorem OAI.DilutedSpinGlass.familyPoisson_count_memLp line 111
7. theorem OAI.DilutedSpinGlass.familyPoisson_count_variance line 117
8. theorem OAI.DilutedSpinGlass.familyPoisson_count_deviation line 125
9. theorem OAI.DilutedSpinGlass.poisson_corrected_score_root_bound line 146

   Source documentation

   The convex concentration estimate instantiated with the literal corrected score of the marked hierarchy and its random-dimensional Poisson root law. The variance premise is precisely the separate Efron--Stein/count estimate.

   theorem poisson_corrected_score_root_bound
       (hm : ∀ i, 0 < m i)
       (hb : ∀ n y, Measurable (fun x => base n x y))
       (hD : ∀ n q y, Measurable (fun x => D n x q y))
       (hE : ∀ n q y, Measurable (fun x => E n x q y))
       (hDb : ∀ n x q y, |D n x q y| ≤ 1)
       (hEb : ∀ n x q y, |E n x q y| ≤ 1)
       {t a b ρ V : ℝ} (ht : |t| ≤ 1/4) (hab : a < b) (hρ : 0 < ρ)
       (hJ : Icc (a-ρ) (b+ρ) ⊆ Ioo (-(1:ℝ)/4) (1/4))
       (hLp : ∀ u ∈ Ioo (-(1:ℝ)/4) (1/4), MemLp (fun z : Sigma X =>
         KernelTower.correctedPerturbLog (T z.1) m (base z.1 z.2) (D z.1 z.2) (E z.1 z.2) t u)
           2 (familyLaw (poissonMeasure r) ν))
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower.correctedPerturbLog, OAI.DilutedSpinGlass.familyLaw

10. theorem OAI.DilutedSpinGlass.familyPoisson_variance_le line 213

    Source documentation

    Efron--Stein plus the independent Poisson count, on the genuine dependent root probability law used by the derivative concentration estimate.

    theorem familyPoisson_variance_le (r : ℝ≥0)
        {F : (n : ℕ) → RootPath I n → ℝ} {A B C D : ℝ}
        (hF : ∀ n, Measurable (F n)) (hb : ∀ n x, |F n x| ≤ A+B*n)
        (hD : 0 ≤ D)
        (hrep : ∀ n (i : Fin n) x y, |F n x-F n (replaceRoot n x i y)| ≤ C)
        (hadd : ∀ n x y, |F (n+1) (x,y)-F n y| ≤ D) :
        variance (fun z : Sigma (RootPath I) => F z.1 z.2)
          (familyLaw (poissonMeasure r) (fun n => rootLaw n (fun _ => μ))) ≤
            (C^2/2+D^2)*(r : ℝ) := by
    …

    Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.replaceRoot, OAI.DilutedSpinGlass.familyLaw, OAI.DilutedSpinGlass.rootLaw

11. theorem OAI.DilutedSpinGlass.correctedMarkedRoot_family_variance line 247

    Source documentation

    The random-count convex correction has its own addition/deletion cost. Replacement of an existing root point is unaffected.

    theorem correctedMarkedRoot_family_variance
        (μ : Measure I) [IsProbabilityMeasure μ] (r : ℝ≥0)
        (T : KernelTower Ω L) (Q : Fin L → FiniteLaw A)
        (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
        (base : FinitePath Ω L → ℝ)
        (factor : I → FinitePath Ω L → FinitePath A L → ℝ)
        (hfmeas : ∀ x y, Measurable (fun i => factor i x y)) {B C : ℝ}
        (hb : ∀ y, |base y| ≤ B) (hC : 0 ≤ C)
        (hf : ∀ i x y, |Real.log (factor i x y)| ≤ C) (c : ℝ) :
        variance (fun z : Sigma (RootPath I) =>
          markedRoot T Q m base (rootArray z.1 z.2) factor+c*z.1)
          (familyLaw (poissonMeasure r) (fun n => rootLaw n (fun _ => μ))) ≤
    …

    Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.markedRoot, OAI.DilutedSpinGlass.rootArray, OAI.DilutedSpinGlass.familyLaw, OAI.DilutedSpinGlass.rootLaw

12. def OAI.DilutedSpinGlass.rootDeviation line 299
13. theorem OAI.DilutedSpinGlass.rootDeviation_nonneg line 302
14. theorem OAI.DilutedSpinGlass.rootDeviation_add_le line 305
15. theorem OAI.DilutedSpinGlass.rootDeviation_smul line 325
16. theorem OAI.DilutedSpinGlass.rootDeviation_sub_le line 329
17. theorem OAI.DilutedSpinGlass.measurable_rootDeviation line 345
18. theorem OAI.DilutedSpinGlass.rootDeviation_bound line 352
19. theorem OAI.DilutedSpinGlass.intervalIntegrable_rootDeviation line 368