OAI/Probability/InvariantIsing/Arrays/NSpinTensorBackwardDerivative.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InvariantIsing.hasDerivAt_logMean_of_bounded_derivative line 16

   Source documentation

   The bounded coordinate derivative gives a local exponential dominator, even when the terminal itself is unbounded.

   lemma hasDerivAt_logMean_of_bounded_derivative
       {A : Type*} [MeasurableSpace A] (μ : Measure A) [IsProbabilityMeasure μ]
       (F D : ℝ → A → ℝ) (hF : ∀ s, Measurable (F s)) (hD : ∀ s, Measurable (D s))
       {K : ℝ} (hK : 0 ≤ K) (hbound : ∀ s a, |D s a| ≤ K)
       (hd : ∀ s a, HasDerivAt (fun q => F q a) (D s a) s)
       {b : ℝ} (hb : b ≠ 0) (t : ℝ)
       (hi : Integrable (fun a => Real.exp (b * F t a)) μ) :
       HasDerivAt (fun s => logMean b μ (F s))
         (∫ a, D t a ∂μ.tilted (fun a => b * F t a)) t := by
   …

2. lemma OAI.InvariantIsing.tensorCascadeBackward_step line 68
3. theorem OAI.InvariantIsing.tensorAncestorMarkKernel_eq_tilted line 81

   Source documentation

   The normalized retained mark transition is exactly the Gaussian tilt by the next actual backward value.

   theorem tensorAncestorMarkKernel_eq_tilted {N m k : ℕ} (hN : 0 < N)
       (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
       (hb : CascadeExponents n b) (i : ℕ) (hi : i < n) (z : SpinTensorIndex I degree → ℝ) :
       tensorAncestorMarkKernel eig U c I degree amplitude n b v i z =
         (tensorGaussianLaw I degree (v i) : Measure (SpinTensorIndex I degree → ℝ)).tilted
           (fun a => b i * tensorCascadeBackward eig U c I degree amplitude n b v (i + 1) (z + a)) := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorAncestorMarkKernel, OAI.InvariantIsing.tensorGaussianLaw, OAI.InvariantIsing.tensorCascadeBackward

4. def OAI.InvariantIsing.tensorCascadeCoordinateMean line 108
5. lemma OAI.InvariantIsing.measurable_tensorCascadeCoordinateMean line 119
6. lemma OAI.InvariantIsing.tensorCascadeCoordinateMean_abs_le line 132
7. lemma OAI.InvariantIsing.tensorCoordinateVariation_add line 150
8. theorem OAI.InvariantIsing.hasDerivAt_tensorCascadeValue_coordinate line 160

   Source documentation

   Every coordinate derivative of the actual backward value is the corresponding mean propagated through the ancestor kernels.

   theorem hasDerivAt_tensorCascadeValue_coordinate {N m k : ℕ} (hN : 0 < N)
       (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
       (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
       (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
       (hb : CascadeExponents n b) (z : SpinTensorIndex I degree → ℝ)
       (j : SpinTensorIndex I degree) (t : ℝ) :
       HasDerivAt (fun s => tensorCascadeValue eig U c I degree amplitude n b v
         (tensorCoordinateVariation I degree z j s))
         (tensorCascadeCoordinateMean eig U c I degree amplitude n b v
           (tensorCoordinateVariation I degree z j t) j) t := by
   …

   Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeValue, OAI.InvariantIsing.tensorCoordinateVariation, OAI.InvariantIsing.tensorCascadeCoordinateMean

9. def OAI.InvariantIsing.tensorBackwardCoordinateMean line 215
10. theorem OAI.InvariantIsing.hasDerivAt_tensorCascadeBackward_coordinate line 225

    Source documentation

    The same derivative identity at every backward level, with the manuscript's ancestor indexing.

    theorem hasDerivAt_tensorCascadeBackward_coordinate {N m k : ℕ} (hN : 0 < N)
        (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
        (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
        (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
        (hb : CascadeExponents n b) (i : ℕ) (z : SpinTensorIndex I degree → ℝ)
        (j : SpinTensorIndex I degree) (t : ℝ) :
        HasDerivAt (fun s => tensorCascadeBackward eig U c I degree amplitude n b v i
          (tensorCoordinateVariation I degree z j s))
          (tensorBackwardCoordinateMean eig U c I degree amplitude n b v i
            (tensorCoordinateVariation I degree z j t) j) t := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorCascadeBackward, OAI.InvariantIsing.tensorCoordinateVariation, OAI.InvariantIsing.tensorBackwardCoordinateMean

11. lemma OAI.InvariantIsing.measurable_tensorBackwardCoordinateMean line 244
12. lemma OAI.InvariantIsing.tensorBackwardCoordinateMean_abs_le line 256
13. theorem OAI.InvariantIsing.tensorBackwardCoordinateMean_step line 272

    Source documentation

    The backward gradient is a martingale under the actual normalized ancestor mark transitions.

    theorem tensorBackwardCoordinateMean_step {N m k : ℕ} (hN : 0 < N)
        (eig : Fin N → ℝ) (U : Rotation N) (c : Fin N → ℝ)
        (I : Fin m → Finset (Fin N)) (degree : Fin k → Fin m → ℕ) (amplitude : Fin k → ℝ)
        (n : ℕ) (b : ℕ → ℝ) (v : ℕ → SpinTensorIndex I degree → ℝ≥0)
        (hb : CascadeExponents n b) (i : ℕ) (hi : i < n)
        (z : SpinTensorIndex I degree → ℝ) (j : SpinTensorIndex I degree) :
        tensorBackwardCoordinateMean eig U c I degree amplitude n b v i z j =
          ∫ a, tensorBackwardCoordinateMean eig U c I degree amplitude n b v (i + 1) (z + a) j
            ∂tensorAncestorMarkKernel eig U c I degree amplitude n b v i z := by
    …

    Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorBackwardCoordinateMean, OAI.InvariantIsing.tensorAncestorMarkKernel