DescentProbability.lean`

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.DFVSGames.Gadget.DescentProbability.noiseFintype line 19
def OAI.DFVSGames.Gadget.DescentProbability.terminalPotential line 25
theorem OAI.DFVSGames.Gadget.DescentProbability.terminalPotential_zero line 30
theorem OAI.DFVSGames.Gadget.DescentProbability.terminalPotential_succ line 38
theorem OAI.DFVSGames.Gadget.DescentProbability.expected_terminal_loss line 51
def OAI.DFVSGames.Gadget.LeafDetection.survivalProbability line 112
def OAI.DFVSGames.Gadget.LeafDetection.detectionProbability line 117
theorem OAI.DFVSGames.Gadget.LeafDetection.detectionProbability_nonneg line 124
theorem OAI.DFVSGames.Gadget.LeafDetection.detectionProbability_restrict_le line 133
theorem OAI.DFVSGames.Gadget.LeafDetection.detectionProbability_zero_of_rank_pos line 144
theorem OAI.DFVSGames.Gadget.LeafDetection.survivalProbability_zero line 169
theorem OAI.DFVSGames.Gadget.LeafDetection.survivalProbability_succ line 179
theorem OAI.DFVSGames.Gadget.LeafDetection.average_child_detection_le line 194
theorem OAI.DFVSGames.Gadget.LeafDetection.half_survival_le_detection line 213
theorem OAI.DFVSGames.Gadget.LeafDetection.quarter_detection_of_terminal_potential line 236
theorem OAI.DFVSGames.Gadget.LeafDetection.quarter_detection_of_restricted_terminal_potential line 249
def OAI.DFVSGames.Gadget.BaseDetection.logicalCharacters line 272
theorem OAI.DFVSGames.Gadget.BaseDetection.traceSpace_logicalCharacters line 277
theorem OAI.DFVSGames.Gadget.BaseDetection.logicalCharacters_finrank line 282
theorem OAI.DFVSGames.Gadget.BaseDetection.theta_pos line 287
theorem OAI.DFVSGames.Gadget.BaseDetection.full_lift_detection line 292
def OAI.DFVSGames.Gadget.Quotient.shiftKernel line 348
abbrev OAI.DFVSGames.Gadget.Quotient.Space line 351
def OAI.DFVSGames.Gadget.Quotient.projection line 353
theorem OAI.DFVSGames.Gadget.Quotient.projection_surjective line 356
theorem OAI.DFVSGames.Gadget.Quotient.mem_shiftKernel line 359
theorem OAI.DFVSGames.Gadget.Quotient.projection_eq_zero line 362
def OAI.DFVSGames.Gadget.Quotient.quotientShift line 373
theorem OAI.DFVSGames.Gadget.Quotient.quotientShift_mk line 379
def OAI.DFVSGames.Gadget.Quotient.logicalShift line 382
theorem OAI.DFVSGames.Gadget.Quotient.logicalShift_lambda line 386
theorem OAI.DFVSGames.Gadget.Quotient.logicalShift_injective line 391
def OAI.DFVSGames.Gadget.Quotient.Equivariant line 403
theorem OAI.DFVSGames.Gadget.Quotient.difference_shift line 406
def OAI.DFVSGames.Gadget.Quotient.conditionedShiftEquiv line 413
def OAI.DFVSGames.Gadget.Quotient.conditionedFiberEquiv line 427
theorem OAI.DFVSGames.Gadget.Quotient.conditioned_fiber_card line 437
theorem OAI.DFVSGames.Gadget.Quotient.output_fiber_card line 444
theorem OAI.DFVSGames.Gadget.Quotient.difference_fiber_card line 450
def OAI.DFVSGames.Gadget.Quotient.conditionedSigmaEquiv line 459
def OAI.DFVSGames.Gadget.Quotient.conditionedProductEquiv line 466
theorem OAI.DFVSGames.Gadget.Quotient.conditionedProductEquiv_fst line 474
theorem OAI.DFVSGames.Gadget.Quotient.conditioned_card_factorization line 480
theorem OAI.DFVSGames.Gadget.Quotient.difference_card_factorization line 488
theorem OAI.DFVSGames.Gadget.Quotient.output_constant_on_fibers line 498
def OAI.DFVSGames.Gadget.Quotient.output line 506
theorem OAI.DFVSGames.Gadget.Quotient.output_projection line 511
theorem OAI.DFVSGames.Gadget.Quotient.output_equivariant line 515
theorem OAI.DFVSGames.Gadget.Quotient.change_iff line 524
theorem OAI.DFVSGames.Gadget.Quotient.character_pullback_shift line 530
theorem OAI.DFVSGames.Gadget.Quotient.detection_iff line 536
def OAI.DFVSGames.Gadget.Quotient.fiberMap line 541
theorem OAI.DFVSGames.Gadget.Quotient.fiberMap_bijective line 548
theorem OAI.DFVSGames.Gadget.Quotient.fiber_card line 561
def OAI.DFVSGames.Gadget.StageQuotient.shifts line 575
def OAI.DFVSGames.Gadget.StageQuotient.shiftEquiv line 577
theorem OAI.DFVSGames.Gadget.StageQuotient.shiftEquiv_coe line 580
theorem OAI.DFVSGames.Gadget.StageQuotient.embed_shiftEquiv_symm line 583
def OAI.DFVSGames.Gadget.StageQuotient.logical line 587
theorem OAI.DFVSGames.Gadget.StageQuotient.logical_shiftEquiv line 590
theorem OAI.DFVSGames.Gadget.StageQuotient.logical_surjective line 594
theorem OAI.DFVSGames.Gadget.StageQuotient.equivariant line 599
abbrev OAI.DFVSGames.Gadget.StageQuotient.Space line 606
def OAI.DFVSGames.Gadget.StageQuotient.projection line 608
theorem OAI.DFVSGames.Gadget.StageQuotient.projection_surjective line 611
instance OAI.DFVSGames.Gadget.StageQuotient.spaceFinite line 614
def OAI.DFVSGames.Gadget.StageQuotient.shift line 617
theorem OAI.DFVSGames.Gadget.StageQuotient.shift_injective line 620
theorem OAI.DFVSGames.Gadget.StageQuotient.shift_logical line 623
def OAI.DFVSGames.Gadget.StageQuotient.output line 629
theorem OAI.DFVSGames.Gadget.StageQuotient.output_projection line 632
theorem OAI.DFVSGames.Gadget.StageQuotient.output_equivariant line 635
def OAI.DFVSGames.Gadget.StageQuotient.noise line 640
theorem OAI.DFVSGames.Gadget.StageQuotient.noise_change_iff line 643
theorem OAI.DFVSGames.Gadget.StageQuotient.character_logical line 648
theorem OAI.DFVSGames.Gadget.StageQuotient.noise_detection_iff line 652
def OAI.DFVSGames.Gadget.StageQuotient.toStage line 657
def OAI.DFVSGames.Gadget.DetectionBridge.IsFullLift line 679
def OAI.DFVSGames.Gadget.DetectionBridge.characterDetection line 683
theorem OAI.DFVSGames.Gadget.DetectionBridge.exists_leftInverse_of_logical_injective line 688
theorem OAI.DFVSGames.Gadget.DetectionBridge.fullLift_of_leftInverse line 693
theorem OAI.DFVSGames.Gadget.DetectionBridge.target_detection_of_full_lift_bound line 701
theorem OAI.DFVSGames.Gadget.DetectionBridge.target_detection_of_retraction_bound line 720
def OAI.DFVSGames.Gadget.QuotientDetection.pullbackFullLift line 749
theorem OAI.DFVSGames.Gadget.QuotientDetection.pullback_detection_iff line 764
theorem OAI.DFVSGames.Gadget.QuotientDetection.full_detection_after_quotient line 777
theorem OAI.DFVSGames.Gadget.QuotientDetection.target_detection_after_quotient line 788