CavityOverlapError.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite-rank overlap errors in cavity coordinates. The retained coordinates cancel exactly; the error is controlled by the special projections and the fixed number of added spins.

def OAI.InvariantIsing.cavityCoordinatePairing line 14
lemma OAI.InvariantIsing.cavityCoordinatePairing_abs_le line 18
def OAI.InvariantIsing.cavityJoinVector line 40
lemma OAI.InvariantIsing.cavityJoinVector_norm_sq line 44
lemma OAI.InvariantIsing.cavity_small_overlap_difference line 49
lemma OAI.InvariantIsing.cavity_normalized_overlap_error_sharp line 62
lemma OAI.InvariantIsing.cavity_normalized_overlap_error line 86

theorem OAI.InvariantIsing.cavity_overlap_error line 97

Source documentation

The local spectral-overlap comparison used in the perturbation interpolation, with a constant depending only on the cavity size.

theorem cavity_overlap_error {N d n : ℕ} (hN : 0 < N)
    (retained : ℝ) (U : Rotation (d + n)) (V : Rotation d)
    (I : Finset (Fin (d + n))) (J : Finset (Fin d))
    (y₁ y₂ : EuclideanSpace ℝ (Fin d)) (ε₁ ε₂ : Spin n)
    (hbase : |(retained + cavityCoordinatePairing V J y₁ y₂) / N| ≤ 1) :
    |(retained + cavityCoordinatePairing U I (cavityJoinVector y₁ ε₁) (cavityJoinVector y₂ ε₂)) /
        (N + n : ℕ) - (retained + cavityCoordinatePairing V J y₁ y₂) / N| ≤
      ((2 * (n : ℝ) + 1) / N) * (1 + ‖y₁‖ ^ 2 + ‖y₂‖ ^ 2) := by
…

Mentions: OAI.InvariantIsing.Rotation, OAI.InvariantIsing.Spin, OAI.InvariantIsing.cavityCoordinatePairing, OAI.InvariantIsing.cavityJoinVector

theorem OAI.InvariantIsing.cavity_total_overlap_extension line 117

Source documentation

Appending n spins changes the total overlap by at most 2n/(N+n).

theorem cavity_total_overlap_extension {N n : ℕ} (hN : 0 < N)
    (σ₁ σ₂ : Spin N) (ε₁ ε₂ : Spin n) :
    |(∑ i : Fin (N + n), spinValue (Fin.append σ₁ ε₁ i) *
        spinValue (Fin.append σ₂ ε₂ i)) / (N + n : ℕ) -
      (∑ i : Fin N, spinValue (σ₁ i) * spinValue (σ₂ i)) / N| ≤
        2 * (n : ℝ) / (N + n) := by
…

Mentions: OAI.InvariantIsing.Spin, OAI.InvariantIsing.spinValue