PrefixProjection.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.polarizedSpec line 14
lemma OAI.DilutedSpinGlass.UniversalDictionary.cast_average line 18
lemma OAI.DilutedSpinGlass.UniversalDictionary.polarized_direction line 23
lemma OAI.DilutedSpinGlass.UniversalDictionary.polarized_anchor line 36

theorem OAI.DilutedSpinGlass.UniversalDictionary.universal_constrained_polarization line 47

Source documentation

Every prescribed sharing history is a finite linear combination of the literal universal dictionary coefficients, with the same old kernel.

theorem universal_constrained_polarization {Ω : Type} [Fintype Ω] {L r k : ℕ}
    (hk : 0 < k) (T : KernelTower Ω (L+1)) (m : Fin (L+2) → ℝ)
    (hm : ∀ j : Fin (L+1), m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last (L+1)) = 1)
    (a b : Fin r → Option (Fin k)) (d : Fin r → Fin L) (spinAnchor : Bool)
    (read : FinitePath Ω (L+1) → Spin)
    (S : PrescribedTree (L+1)) (anchorLeaf : S.Leaf) (f : PrescribedTree.Sample Ω S → ℝ) :
    PrescribedTree.constrainedHistory T m a b (fun j => (d j).castSucc)
      (fun c x =>
        match c with
        | none => if spinAnchor then spin (read x) else 1
        | some _ => spin (read x)) S anchorLeaf f =
    ((k:ℝ)^k / 2^k) * ∑ ε : Fin k → Bool, (∏ j, Polarization.sign (ε j)) *
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory, OAI.DilutedSpinGlass.spin, OAI.DilutedSpinGlass.Polarization.sign

theorem OAI.DilutedSpinGlass.UniversalDictionary.universal_analytic_selection line 96

Source documentation

The physical family is now fixed once and for all. Its rational auxiliary mark dictionary simultaneously contains every finite signed polarization and both spin and marker anchors, without changing any old reservoir for new probes.

theorem universal_analytic_selection {L p : ℕ} (m : Fin (L+1) → ℝ)
    (M : Model p) {C H c : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H) (hc : 0 < c)
    (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ| ≤ C)
    (hh : ∀ᵐ h ∂M.field.toMeasure, |h| ≤ H)
    (hθi : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
    (hhi : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
    (hm : ∀ l, c ≤ m l) (hmono : Monotone m) (hend : m (Fin.last L) = 1)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ), StrictMono Ns ∧
      (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
      (∀ n, ConcreteReservoir.increment (weights L) prior m direction anchor M (Ns n) (us n) ≤
        liminf (pressure M) atTop+ε) ∧
…

Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh, OAI.DilutedSpinGlass.ConcreteReservoir.increment, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure

def OAI.DilutedSpinGlass.PrescribedTree.treeOverlap line 130
Source documentation
The normalized product of all leaves, with the exact zero-size convention.
```
noncomputable def treeOverlap (S : PrescribedTree n) (f : FinitePath Ω n → Fin N → ℝ)
    (z : Sample Ω S) : ℝ := (∑ i, leafProduct S (fun x => f x i) z)/(N:ℝ)
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.leafProduct
lemma OAI.DilutedSpinGlass.PrescribedTree.treeOverlap_bound line 134
lemma OAI.DilutedSpinGlass.PrescribedTree.treeOverlap_unary line 142
def OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt line 149
Source documentation
Proper-child covariance at the later first split, retaining the entire original evaluation prefix. These are genuine iterated kernel expectations.
```
noncomputable def descendantEnergyAt (C : PrescribedTree n) (r : ℕ) : (d : ℕ) →
    KernelTower Ω (n+1+r+1+d) → (FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) → ℝ
  | 0,T,f => shapeEnergyAt C (r+1) T f
  | d+1,T,f => T.1.expect (fun x => descendantEnergyAt C r d (T.2 x) (fun y => f (x,y)))
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt
lemma OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt_nonneg line 154
lemma OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError_prefixed_sq line 163
Source documentation
Exact identification of the old error in the signed identity with the conditional two-copy error of the whole multileaf shape, at arbitrary d.
```
lemma oldProjectionError_prefixed_sq (S : PrescribedTree n) (a : S.Leaf) (d : ℕ)
    (T : KernelTower Ω (n+1+d)) (f X : FinitePath Ω (n+1+d) → Fin N → ℝ) :
    (oldProjectionError (stem (doubled S) d) T (stemLeaf (doubled S) d ⟨0,a⟩)
      (stemLeaf (doubled S) d ⟨1,a⟩) (treeOverlap (stem (doubled S) d) f) X)^2 =
      shapeProjectionSqAt S a d T f X := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.stemLeaf, OAI.DilutedSpinGlass.PrescribedTree.treeOverlap, OAI.DilutedSpinGlass.PrescribedTree.shapeProjectionSqAt
theorem OAI.DilutedSpinGlass.PrescribedTree.prefixed_stem_projection_sq_le line 201
Source documentation
The projection energy uses only proper-child energies even when the first evaluation depth is not the root. No prefix is discarded.
```
theorem prefixed_stem_projection_sq_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r d : ℕ) (T : KernelTower Ω (n+1+r+1+d))
    (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i| ≤ 1) :
    shapeProjectionSqAt (stem (.node k C) r) (stemLeaf (.node k C) r a) d T f
      (fun x i => splitProjector (.node k C) r d T (fun y => f y i) x) ≤
      4*(k:ℝ)*∑ i, Real.sqrt (descendantEnergyAt (C i) r d T f) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.shapeProjectionSqAt, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.stemLeaf, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt
theorem OAI.DilutedSpinGlass.PrescribedTree.prefixed_stem_covariance_three_copy_le line 223
Source documentation
The exact actual whole-shape covariance with both evaluation and first split at arbitrary depths, bounded by the full projected three-copy term.
```
theorem prefixed_stem_covariance_three_copy_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r d : ℕ) (T : KernelTower Ω (n+1+r+1+d))
    (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i| ≤ 1) :
    shapeEnergyAt (stem (.node k C) r) d T f ≤
      2*KernelTower.halfTripleDifferenceAt (n+1+r+1+d) T d
        (fun x i => splitProjector (.node k C) r d T (fun y => f y i) x)+
      16*(k:ℝ)*∑ i, Real.sqrt (descendantEnergyAt (C i) r d T f) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.KernelTower.halfTripleDifferenceAt, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt
theorem OAI.DilutedSpinGlass.PrescribedTree.prefixed_stem_old_error_le line 238
Source documentation
The L2 old-test error in the prescribed-tree identity, not merely a projected covariance, now has its explicit proper-child bound.
```
theorem prefixed_stem_old_error_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r d : ℕ) (T : KernelTower Ω (n+1+r+1+d))
    (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i| ≤ 1) :
    let S := stem (.node k C) r
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.stem