Documentation

Anderson4D.Main.CouplingThreshold

A common small-coupling threshold #

The final argument uses three independently selected positive power constants. This file chooses one positive coupling threshold which is simultaneously inside the external Proposition 3.6 range, closes the second-moment geometric series, and places both good-event ratios below the fixed boundary ratio.

source
noncomputable def Anderson4D.Prop36Family.mainCouplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) (secondPower goodPower Crenorm : ℝ) :
ℝ

A single coupling threshold for the external coefficient input, the second-moment geometric series, and the two good-event geometric ratios.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Anderson4D.Prop36Family.mainCouplingThreshold_pos {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) :
    0 < h.mainCouplingThreshold secondPower goodPower Crenorm

    The common threshold is positive whenever its three named power constants are positive.

    source
    theorem Anderson4D.Prop36Family.mainCouplingThreshold_spec {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm lam : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hlam : lam ∈ Set.Ioo 0 (h.mainCouplingThreshold secondPower goodPower Crenorm)) :
    lam ∈ Set.Ioo 0 h.couplingThreshold ∧ secondPower * lam < 1 ∧ lam ≤ 1 ∧ goodPower * lam ≤ PartialPairing.boundaryGeometricRatio ∧ Crenorm * lam ≤ PartialPairing.boundaryGeometricRatio

    Every coupling in the common range satisfies all five numerical requirements used by the final assembly.

    source
    theorem Anderson4D.Prop36Family.mem_couplingThreshold_of_mem_mainCouplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm lam : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hlam : lam ∈ Set.Ioo 0 (h.mainCouplingThreshold secondPower goodPower Crenorm)) :
    lam ∈ Set.Ioo 0 h.couplingThreshold

    The common range is contained in the external Proposition 3.6 range.

    source
    theorem Anderson4D.Prop36Family.secondPower_mul_lt_one_of_mem_mainCouplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm lam : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hlam : lam ∈ Set.Ioo 0 (h.mainCouplingThreshold secondPower goodPower Crenorm)) :
    secondPower * lam < 1

    The second-moment geometric ratio is strictly subcritical on the common range.

    source
    theorem Anderson4D.Prop36Family.le_one_of_mem_mainCouplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm lam : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hlam : lam ∈ Set.Ioo 0 (h.mainCouplingThreshold secondPower goodPower Crenorm)) :
    lam ≤ 1

    Couplings in the common range are at most one.

    source
    theorem Anderson4D.Prop36Family.goodPower_mul_le_boundaryGeometricRatio_of_mem_mainCouplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm lam : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hlam : lam ∈ Set.Ioo 0 (h.mainCouplingThreshold secondPower goodPower Crenorm)) :
    goodPower * lam ≤ PartialPairing.boundaryGeometricRatio

    The good-event power ratio lies below the fixed boundary ratio on the common range.

    source
    theorem Anderson4D.Prop36Family.Crenorm_mul_le_boundaryGeometricRatio_of_mem_mainCouplingThreshold {M : NoiseModel} {ρ : SmoothCutoff} (h : Prop36Family M ρ) {secondPower goodPower Crenorm lam : ℝ} (hsecond : 0 < secondPower) (hgood : 0 < goodPower) (hCrenorm : 0 < Crenorm) (hlam : lam ∈ Set.Ioo 0 (h.mainCouplingThreshold secondPower goodPower Crenorm)) :
    Crenorm * lam ≤ PartialPairing.boundaryGeometricRatio

    The renormalization ratio lies below the fixed boundary ratio on the common range.