OAI/Probability/InvariantIsing/Arrays/NSpinTensorProjectedBackward.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.rotationCoordinate line 14
2. lemma OAI.InvariantIsing.rotation_apply_coordinates line 17
3. def OAI.InvariantIsing.tensorBackwardProjectedMean line 32
4. lemma OAI.InvariantIsing.tensorBackwardProjectedMean_eq line 39
5. def OAI.InvariantIsing.tensorProjectedCoordinateCap line 48
6. lemma OAI.InvariantIsing.measurable_tensorBackwardProjectedMean line 52
7. lemma OAI.InvariantIsing.tensorBackwardProjectedMean_abs_le line 61
8. lemma OAI.InvariantIsing.integrable_tensorBackwardProjectedMean line 76
9. theorem OAI.InvariantIsing.tensorBackwardProjectedMean_step line 90
10. lemma OAI.InvariantIsing.tensorBackwardProjectedMean_terminal line 118
11. def OAI.InvariantIsing.tensorProjectedPairPayoff line 128
12. lemma OAI.InvariantIsing.tensorProjectedPairPayoff_cons line 138
13. lemma OAI.InvariantIsing.integral_pair_product_sum line 148
14. theorem OAI.InvariantIsing.tensorAncestorPairPathMean_independent_projected line 161
15. def OAI.InvariantIsing.tensorSharedProjectedProduct line 214
16. lemma OAI.InvariantIsing.tensorSharedProjectedProduct_nonneg line 230
17. theorem OAI.InvariantIsing.tensorAncestorPairPathMean_projected line 244
18. lemma OAI.InvariantIsing.tensorPairPathSpinMean_projectedPayoff line 277
19. theorem OAI.InvariantIsing.tensorProjectedOverlap_backward_identity line 292

    Source documentation

    The actual projected-overlap test is the shared-path expectation of products of projected backward gradients at the branching level.

    theorem tensorProjectedOverlap_backward_identity (hpub : PanchenkoTalagrandTensorPairInput)
        {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) (J : Finset (Fin N)) (z : SpinTensorIndex I degree → ℝ)
        (ψ : ℕ → ℝ) {B : ℝ} (hB : 0 ≤ B) (hψ : ∀ d, |ψ d| ≤ B) :
        tensorSpinPairAverage eig U c I degree amplitude n b v z ψ
          (fun σ => projectedOverlap U J (σ 0) (σ 1)) =
          ∫ α : ℕ → LabeledLeaf n, ψ (labeledCommonDepth n (α 0) (α 1)) *
            tensorSharedProjectedProduct eig U c I degree amplitude n b v J
              (labeledCommonDepth n (α 0) (α 1)) n 0 z z ∂cascadeReplicaLaw n b := by
    …

    Mentions: OAI.InvariantIsing.PanchenkoTalagrandTensorPairInput, OAI.InvariantIsing.Rotation, OAI.InvariantIsing.SpinTensorIndex, OAI.InvariantIsing.tensorSpinPairAverage, OAI.InvariantIsing.projectedOverlap, OAI.InvariantIsing.tensorSharedProjectedProduct

20. theorem OAI.InvariantIsing.tensorProjectedOverlap_nonneg line 313
21. theorem OAI.InvariantIsing.tensorRootedProjectedOverlap_backward_identity line 326