of_split

formal source

 785namespace ExportForcesPaymentHypothesis
 786
 787/-- Build the export→payment bookkeeping lemma from the three abstract implication interfaces. -/
 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
 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)