OAI/Computability/MinUncut/Estimates/CoupledAnswer.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MinUncut.Inner.coupledAnswerline 25 - def
OAI.MinUncut.Inner.secondFailureline 29 - def
OAI.MinUncut.Inner.secondRejectionline 34 - lemma
OAI.MinUncut.Inner.coupledAnswer_measurableline 38 - lemma
OAI.MinUncut.Inner.coupledAnswer_memLpline 43 - lemma
OAI.MinUncut.Inner.secondFailure_eqline 50 - lemma
OAI.MinUncut.Inner.coupled_score_integrableline 57 - lemma
OAI.MinUncut.Inner.gradient_coupled_scoreline 64 - theorem
OAI.MinUncut.Inner.gradient_second_comparisonline 71