OAI/Analysis/HenonEmden/LayerAssembly.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.LayerPressure.sourceWeight line 17
  2. def OAI.HenonLaneEmden.LayerPressure.sourceLower line 21
  3. def OAI.HenonLaneEmden.LayerPressure.sourceUpper line 23
  4. lemma OAI.HenonLaneEmden.LayerPressure.measurable_sourceWeight line 27
  5. lemma OAI.HenonLaneEmden.LayerPressure.measurable_sourceLower line 42
  6. lemma OAI.HenonLaneEmden.LayerPressure.measurable_sourceUpper line 47
  7. lemma OAI.HenonLaneEmden.LayerPressure.sourceWeight_nonneg line 53
  8. lemma OAI.HenonLaneEmden.LayerPressure.sourceWeight_le line 57
  9. def OAI.HenonLaneEmden.LayerPressure.splitKernel line 61
  10. def OAI.HenonLaneEmden.LayerPressure.splitDirection line 63
  11. lemma OAI.HenonLaneEmden.LayerPressure.measurable_splitKernel line 66
  12. lemma OAI.HenonLaneEmden.LayerPressure.measurable_splitDirection line 69
  13. def OAI.HenonLaneEmden.LayerPressure.pairLeft line 73
  14. def OAI.HenonLaneEmden.LayerPressure.pairRight line 77
  15. lemma OAI.HenonLaneEmden.LayerPressure.measurable_pairLeft line 86
  16. lemma OAI.HenonLaneEmden.LayerPressure.measurable_pairRight line 95
  17. lemma OAI.HenonLaneEmden.LayerPressure.weighted_leftAverage_eq line 110
  18. lemma OAI.HenonLaneEmden.LayerPressure.weighted_rightAverage_eq line 125
  19. lemma OAI.HenonLaneEmden.LayerPressure.pair_line_comparison line 140
  20. lemma OAI.HenonLaneEmden.LayerPressure.ae_distinct_transverse line 162
  21. lemma OAI.HenonLaneEmden.LayerPressure.global_nonnegative_pressure line 173

    Source documentation

    The globally integrated nonnegative interval comparison. No source, endpoint, or energy integrability is assumed; all terms are still extended values.

    lemma global_nonnegative_pressure (μ : Measure Z) [SFinite μ] [NullSingletonClass μ]
    (n : ℕ) (hn : 3 ≤ n) {C : ℝ} (hC : 0 ≤ C)
    {f g h d : Z × ℝ → ℝ} (hf : Measurable f) (hg : Measurable g)
    (hfo : IsOpen (parameterLayer f)) (hgo : IsOpen (parameterLayer g))
    (hh : Continuous h) (hd : Continuous d) (hhn : ∀ x, 0 ≤ h x) (δ : ℝ) :
    (∫⁻ z, ENNReal.ofReal (pairLeft n C f g h d δ z)
      ∂(layerMeasure (μ.prod volume) f).prod (layerMeasure (μ.prod volume) g)) ≤
    ∫⁻ z, ENNReal.ofReal (pairRight n C f g h d δ z)
      ∂(layerMeasure (μ.prod volume) f).prod (layerMeasure (μ.prod volume) g) := by
…

    Mentions: OAI.HenonLaneEmden.LayerPressure.pairLeft, OAI.HenonLaneEmden.LayerPressure.pairRight