theorem
proved
term proof
of_split
show as:
view Lean formalization →
formal statement (Lean)
788theorem of_split
789 {ExportEvent ForcingEvent NegativeSigmaEvent ConcavityEvent AbsorptionClass : ℝ → ℝ → Prop}
790 (P : Payments)
791 (hSplit : ExportSplitHypothesis ExportEvent ForcingEvent NegativeSigmaEvent ConcavityEvent)
792 (hForcing : NoRigidRotationAbsorptionHypothesis ForcingEvent AbsorptionClass P)
793 (hNeg : NegativeSigmaForcesBandPaymentHypothesis NegativeSigmaEvent P) :
794 ExportForcesPaymentHypothesis ExportEvent AbsorptionClass ConcavityEvent P := by
proof body
Term-mode proof.
795 classical
796 rcases hForcing.exists_c with ⟨cF, hcF_pos, hcF⟩
797 rcases hNeg.exists_c with ⟨cN, hcN_pos, hcN⟩
798 refine ⟨min cF cN, lt_min hcF_pos hcN_pos, ?_⟩
799 intro ε r hε hr hExport
800 have hcases := hSplit.split ε r hε hr hExport
801 rcases hcases with hF | hrest
802 · -- forcing channel
803 have hF' := hcF ε r hε hr hF
804 rcases hF' with hPay | hAbs
805 · left
806 have hmin : min cF cN ≤ cF := min_le_left _ _
807 exact (mul_le_mul_of_nonneg_right hmin (sq_nonneg ε)).trans hPay
808 · right
809 exact Or.inl hAbs
810 · rcases hrest with hNegEvent | hConc
811 · -- negative-sigma channel gives band payment, hence total payment
812 have hRho : cN * (ε ^ 2) ≤ P.payRho r := hcN ε r hε hr hNegEvent
813 left
814 have hmin : min cF cN ≤ cN := min_le_right _ _
815 have : min cF cN * (ε ^ 2) ≤ cN * (ε ^ 2) :=
816 mul_le_mul_of_nonneg_right hmin (sq_nonneg ε)
817 have hRho' : P.payRho r ≤ P.payXi r + P.payRho r :=
818 le_add_of_nonneg_left (P.payXi_nonneg r)
819 exact this.trans (hRho.trans hRho')
820 · right
821 exact Or.inr hConc
822
823end ExportForcesPaymentHypothesis
824
825/-- **K-ODE interface (step 1):** absorption-class ⇒ quantitative affine ansatz on a smaller cylinder.
826
827At the spec layer, both “absorption class” and “affine ansatz class” are abstract predicates on `(ε,r)`. -/