No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
52structure ErrorModel where
53 p_I : ℝ -- Probability of no error
54 p_X : ℝ -- Probability of bit flip
55 p_Y : ℝ -- Probability of Y error
56 p_Z : ℝ -- Probability of phase flip
57 nonneg_I : p_I ≥ 0
58 nonneg_X : p_X ≥ 0
59 nonneg_Y : p_Y ≥ 0
60 nonneg_Z : p_Z ≥ 0
61 normalized : p_I + p_X + p_Y + p_Z = 1
62
63/-- The depolarizing channel with error probability p.
64 All errors equally likely. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
depolarizing
in IndisputableMonolith.Information.QuantumErrorCorrection
decl_use
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
probability
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
depolarizing
in IndisputableMonolith.Information.QuantumErrorCorrection
decl_use
-
normalized
in IndisputableMonolith.NavierStokes.RunningMaxNormalization
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use
-
probability
in IndisputableMonolith.QFT.SMatrixUnitarity
decl_use
-
probability
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use