OAI/Analysis/HenonEmden/LayerSplit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HenonLaneEmden.LayerTonelli.tripleSwap line 15
  2. lemma OAI.HenonLaneEmden.LayerTonelli.tripleSwap_apply line 21
  3. lemma OAI.HenonLaneEmden.LayerTonelli.measurePreserving_tripleSwap line 25
  4. def OAI.HenonLaneEmden.LayerTonelli.parameterLayer line 35
  5. lemma OAI.HenonLaneEmden.LayerTonelli.measurableSet_parameterLayer line 38
  6. def OAI.HenonLaneEmden.LayerTonelli.parameterLayerMeasure line 43
  7. instance OAI.HenonLaneEmden.LayerTonelli.parameterLayerMeasure_sfinite line 47
  8. lemma OAI.HenonLaneEmden.LayerTonelli.measurePreserving_layer_tripleSwap line 50
  9. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_layer_split line 60

    Source documentation

    After permuting the real position and level coordinates, every pair layer integral is the iterated nonnegative integral over two transverse/level parameters and then the two real line layers. This is valid before proving finiteness.

    lemma lintegral_pair_layer_split (μ : Measure Z) [SFinite μ]
    {f g : Z × ℝ → ℝ} (hf : Measurable f) (hg : Measurable g)
    {F : ((Z × ℝ) × ℝ) × ((Z × ℝ) × ℝ) → ℝ≥0∞} (hF : Measurable F) :
    (∫⁻ z, F z ∂(layerMeasure (μ.prod volume) f).prod (layerMeasure (μ.prod volume) g)) =
      ∫⁻ p : (Z × ℝ) × (Z × ℝ),
        ∫⁻ s : ℝ × ℝ in {s | (p.1,s) ∈ parameterLayer f} ×ˢ {s | (p.2,s) ∈ parameterLayer g},
          F (((p.1.1,s.1),p.1.2),((p.2.1,s.2),p.2.2))
        ∂volume.prod volume ∂(μ.prod volume).prod (μ.prod volume) := by
…

    Mentions: OAI.HenonLaneEmden.LayerTonelli.layerMeasure, OAI.HenonLaneEmden.LayerTonelli.parameterLayer