OAI/Probability/DilutedSpin/ProductEvaluationContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.stemMeanAt_bound line 11
2. def OAI.DilutedSpinGlass.PrescribedTree.productStemIncrementSq line 24

   Source documentation

   The actual change of a product of proper-child conditional means, when its common evaluation depth advances by one on the SAME full sampled path.

   noncomputable def productStemIncrementSq {ι : Type*} [Fintype ι]
       (C : ι → PrescribedTree n) (r : ℕ) (T : KernelTower Ω (n+r))
       (f : FinitePath Ω (n+r) → ℝ) (d : Fin r) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath

3. lemma OAI.DilutedSpinGlass.PrescribedTree.productStemIncrementSq_nonneg line 31
4. lemma OAI.DilutedSpinGlass.PrescribedTree.productStemIncrementSq_le line 37
5. theorem OAI.DilutedSpinGlass.PrescribedTree.sum_productStemIncrementSq_le line 52

   Source documentation

   Finite product martingale-energy bound. Only the number of proper children occurs in the constant, not the depth, dimension or kernels.

   theorem sum_productStemIncrementSq_le {ι : Type*} [Fintype ι]
       (C : ι → PrescribedTree n) (r : ℕ) (T : KernelTower Ω (n+r))
       (f : FinitePath Ω (n+r) → ℝ) (hf : ∀ x, |f x|≤1) :
       (∑ d : Fin r, productStemIncrementSq C r T f d) ≤ (Fintype.card ι:ℝ)^2 := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.productStemIncrementSq

6. theorem OAI.DilutedSpinGlass.PrescribedTree.averaged_productStemIncrement_spatial_le line 69

   Source documentation

   The evaluation-depth component of the manuscript's h_N error, with its literal 1/L normalization and spatial average. Zero spatial size is included.

   theorem averaged_productStemIncrement_spatial_le {ι : Type*} [Fintype ι]
       (C : ι → PrescribedTree n) (r L : ℕ) (U : Finset (Fin r))
       (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → Fin N → ℝ)
       (hf : ∀ x j, |f x j|≤1) :
       ((∑ d ∈ U, (∑ j : Fin N, productStemIncrementSq C r T (fun x => f x j) d)/(N:ℝ))/(L:ℝ)) ≤
         (Fintype.card ι:ℝ)^2/(L:ℝ) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.productStemIncrementSq