OAI/Analysis/HenonEmden/Tonelli.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.LayerTonelli.sourceSubgraph line 16

   Source documentation

   The literal positive source subgraph; no integrability is implicit.

   def sourceSubgraph (f : E → ℝ) : Set (E × ℝ) := {z | 0 < z.2 ∧ z.2 < f z.1}

2. lemma OAI.HenonLaneEmden.LayerTonelli.measurableSet_sourceSubgraph line 18
3. def OAI.HenonLaneEmden.LayerTonelli.layerMeasure line 23
4. instance OAI.HenonLaneEmden.LayerTonelli.layerMeasure_sfinite line 26
5. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_layerMeasure line 29
6. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_layerMeasure_fst line 41
7. def OAI.HenonLaneEmden.LayerTonelli.potential line 51

   Source documentation

   Newton potentials are kept as nonnegative extended integrals until their finiteness has separately been supplied by the PDE.

   noncomputable def potential (μ : Measure E) (k : E × E → ℝ≥0∞) (g : E → ℝ) (x : E) : ℝ≥0∞ :=
   …

8. lemma OAI.HenonLaneEmden.LayerTonelli.measurable_potential line 54
9. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_layer_kernel line 59
10. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_endpoint line 66

    Source documentation

    This is the Tonelli recovery at an arbitrary measurable selected endpoint. The selected point depends only on the first layer, never on the second layer.

    lemma lintegral_pair_endpoint (μ : Measure E) [SFinite μ] {f g : E → ℝ}
        {k : E × E → ℝ≥0∞} {a : E × ℝ → ℝ≥0∞} {endpoint : E × ℝ → E}
        (hg : Measurable g) (hk : Measurable k) (ha : Measurable a) (he : Measurable endpoint) :
        ∫⁻ z, a z.1*k (endpoint z.1,z.2.1) ∂(layerMeasure μ f).prod (layerMeasure μ g) =
          ∫⁻ z, a z*potential μ k g (endpoint z) ∂layerMeasure μ f := by
    …

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

11. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_position line 78
12. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_endpoint_average line 85
13. lemma OAI.HenonLaneEmden.LayerTonelli.lintegral_pair_spatial line 106

    Source documentation

    Integrating any spatial nonnegative pair function over the two sets of levels gives exactly the interaction with both source densities.

    lemma lintegral_pair_spatial (μ : Measure E) [SFinite μ] {f g : E → ℝ}
        {F : E × E → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) (hF : Measurable F) :
        ∫⁻ z, F (z.1.1,z.2.1) ∂(layerMeasure μ f).prod (layerMeasure μ g) =
          ∫⁻ z, ENNReal.ofReal (f z.1)*ENNReal.ofReal (g z.2)*F z ∂μ.prod μ := by
    …

    Mentions: OAI.HenonLaneEmden.LayerTonelli.layerMeasure