module
module
IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSectionReadout
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (14)
-
structure
JointSectionReadout -
theorem
isAmplitudeLinear_channel_of_sectionReadout -
theorem
channel_eq_zero_of_density_only_of_sectionReadout -
theorem
not_exists_nontrivial_density_only_channel_with_sectionReadout -
def
sectionReadout_of_pureTensorFactorization -
theorem
isAmplitudeLinear_channel_of_pureTensorFactorization_via_sectionReadout -
structure
RecognitionSectionReadout -
theorem
isAmplitudeLinear_channel_of_recognitionSectionReadout -
theorem
channel_eq_zero_of_density_only_of_recognitionSectionReadout -
theorem
not_exists_nontrivial_density_only_channel_with_recognitionSectionReadout -
structure
SectionReadoutForcingCert -
def
sectionReadoutForcingCert -
theorem
sectionReadoutForcingCert_inhabited -
theorem
factor_product_retirement_one_statement