OAI/Analysis/HenonEmden/PressureRecovery.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_endpoint_right line 14
  2. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_position_right line 25
  3. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_endpoint_average_right line 33
  4. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_weight_sum line 47
  5. lemma OAI.HenonLaneEmden.LayerPressure.splitKernel_symm line 66
  6. lemma OAI.HenonLaneEmden.LayerPressure.splitKernel_nonneg line 73
  7. lemma OAI.HenonLaneEmden.LayerPressure.pairLeft_recovery line 76
  8. lemma OAI.HenonLaneEmden.LayerPressure.pressure_cancellation line 102

    Source documentation

    Finite cancellation is used only after the endpoint contributions have been proved finite.

    lemma pressure_cancellation {U V R P M Q L T : ℝ≥0∞} (hV : V ≠ ⊤)
    (hcomp : U ≤ V+P+M) (hrec : R+V ≤ U+L+T) (hmis : M ≤ Q+L) :
    R ≤ P+Q+2*L+T := by
…