KernelTower.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.FinitePath line 13
Source documentation
A finite path space. All probability kernels in the bounded auxiliary perturbation construction are finite, conditional on the physical root.
```
def FinitePath (Ω : Type) : ℕ → Type
  | 0 => Unit
  | n + 1 => Ω × FinitePath Ω n
```
instance OAI.DilutedSpinGlass.finitePathFintype line 17

def OAI.DilutedSpinGlass.KernelTower line 24

Source documentation

Finite kernels depending on the full preceding path, before tilting.

def KernelTower (Ω : Type) [Fintype Ω] : ℕ → Type
  | 0 => Unit
  | n + 1 => FiniteLaw Ω × (Ω → KernelTower Ω n)

namespace KernelTower

variable {Ω : Type} [Fintype Ω]

Mentions: OAI.DilutedSpinGlass.FiniteLaw

def OAI.DilutedSpinGlass.KernelTower.unitLaw line 32
def OAI.DilutedSpinGlass.KernelTower.law line 37
def OAI.DilutedSpinGlass.KernelTower.backwardLog line 41
def OAI.DilutedSpinGlass.KernelTower.tilt line 47
theorem OAI.DilutedSpinGlass.KernelTower.expect_unitLaw line 55
theorem OAI.DilutedSpinGlass.KernelTower.law_zero_expect line 58
theorem OAI.DilutedSpinGlass.KernelTower.law_succ_expect line 61
theorem OAI.DilutedSpinGlass.KernelTower.hasDerivAt_backwardLog line 68
Source documentation
First variation through the entire finite hierarchy, with all exponents and all original path-dependent priors retained.
```
theorem hasDerivAt_backwardLog (n : ℕ) (T : KernelTower Ω n)
    (m : Fin n → ℝ) (hm : ∀ i, m i ≠ 0)
    {f : ℝ → FinitePath Ω n → ℝ} {f' : FinitePath Ω n → ℝ} {u : ℝ}
    (hf : ∀ x, HasDerivAt (fun t => f t x) (f' x) u) :
    HasDerivAt (fun t => backwardLog n T m (f t))
      ((law n (tilt n T m (f u))).expect f') u := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.backwardLog, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.KernelTower.tilt
theorem OAI.DilutedSpinGlass.KernelTower.insertion line 86
def OAI.DilutedSpinGlass.KernelTower.varianceEnergy line 110
theorem OAI.DilutedSpinGlass.KernelTower.varianceEnergy_lower line 122
Source documentation
The lower energy estimate in pert:second-derivative; the smallest exponent controls the full terminal path variance, not merely the root variance.
```
theorem varianceEnergy_lower (n : ℕ) (T : KernelTower Ω n)
    (m : Fin n → ℝ) {c : ℝ} (hm : ∀ i, c ≤ m i) (f : FinitePath Ω n → ℝ) :
    c * (law n T).covariance f f ≤ varianceEnergy n T m f := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.KernelTower.varianceEnergy
theorem OAI.DilutedSpinGlass.KernelTower.varianceEnergy_const line 142
Source documentation
The exact martingale-energy telescoping identity.
```
theorem varianceEnergy_const (n : ℕ) (T : KernelTower Ω n) (c : ℝ)
    (f : FinitePath Ω n → ℝ) :
    varianceEnergy n T (fun _ => c) f = c * (law n T).covariance f f := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.varianceEnergy, OAI.DilutedSpinGlass.KernelTower.law

theorem OAI.DilutedSpinGlass.KernelTower.hasDerivAt_path_score line 156

Source documentation

Second variation through a tower. Terminal derivatives plus the positive weighted martingale energy from every depth. No concentration is assumed.

theorem hasDerivAt_path_score (n : ℕ) (T : KernelTower Ω n)
    (m : Fin n → ℝ) (hm : ∀ i, m i ≠ 0)
    {f f' : ℝ → FinitePath Ω n → ℝ} {f'' : FinitePath Ω n → ℝ} {u : ℝ}
    (hf : ∀ x, HasDerivAt (fun t => f t x) (f' u x) u)
    (hf' : ∀ x, HasDerivAt (fun t => f' t x) (f'' x) u) :
    HasDerivAt (fun t => (law n (tilt n T m (f t))).expect (f' t))
      ((law n (tilt n T m (f u))).expect f'' +
        varianceEnergy n (tilt n T m (f u)) m (f' u)) u := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.KernelTower.varianceEnergy

theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_add line 178
Source documentation
Root-measurable homogeneous shifts pass through the whole backward recursion.
```
theorem backwardLog_add (n : ℕ) (T : KernelTower Ω n) (m : Fin n → ℝ)
    (hm : ∀ i, m i ≠ 0) (f : FinitePath Ω n → ℝ) (c : ℝ) :
    backwardLog n T m (fun x => f x + c) = backwardLog n T m f + c := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.backwardLog
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_const line 192
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_stability line 205
Source documentation
The uniform insertion bound, with full arbitrary depth-dependent priors.
```
theorem backwardLog_stability (n : ℕ) (T : KernelTower Ω n) (m : Fin n → ℝ)
    (hm : ∀ i, 0 < m i) {f g : FinitePath Ω n → ℝ} {c : ℝ}
    (hfg : ∀ x, |f x - g x| ≤ c) :
    |backwardLog n T m f - backwardLog n T m g| ≤ c := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.backwardLog
theorem OAI.DilutedSpinGlass.KernelTower.backwardLog_bound line 217
Source documentation
Pointwise bounds survive every backward step, uniformly in depth.
```
theorem backwardLog_bound (n : ℕ) (T : KernelTower Ω n) (m : Fin n → ℝ)
    (hm : ∀ i, 0 < m i) {f : FinitePath Ω n → ℝ} {c : ℝ}
    (hf : ∀ x, |f x| ≤ c) : |backwardLog n T m f| ≤ c := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.backwardLog
theorem OAI.DilutedSpinGlass.KernelTower.tilt_insertion line 226
Source documentation
Updated kernels after an insertion agree with the successive tilting of all the old tilted kernels. This is tree:updated-kernel at every depth.
```
theorem tilt_insertion (n : ℕ) (T : KernelTower Ω n) (m : Fin n → ℝ)
    (f a : FinitePath Ω n → ℝ) :
    tilt n (tilt n T m f) m a = tilt n T m (fun x => f x + a x) := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.tilt
theorem OAI.DilutedSpinGlass.KernelTower.continuousOn_backwardLog line 244
theorem OAI.DilutedSpinGlass.KernelTower.continuousOn_path_expect line 254
theorem OAI.DilutedSpinGlass.KernelTower.continuousOn_varianceEnergy_tilt line 267
theorem OAI.DilutedSpinGlass.KernelTower.second_variation_lower line 284
theorem OAI.DilutedSpinGlass.KernelTower.thermal_variance_integral line 295