OAI/Analysis/HenonEmden/CapWeights.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HenonLaneEmden.CapWeights.profile line 18

   Source documentation

   A Lipschitz tent profile suffices for the pressure argument; no derivative of the profile is used in the layer or interval integration.

   def profile (θ : T) (l : ℝ) (e : T) : ℝ := max (1-dist e θ/l) 0

2. lemma OAI.HenonLaneEmden.CapWeights.profile_nonneg line 20
3. lemma OAI.HenonLaneEmden.CapWeights.profile_le_one line 21
4. lemma OAI.HenonLaneEmden.CapWeights.profile_eq_zero line 25
5. lemma OAI.HenonLaneEmden.CapWeights.profile_half line 32
6. lemma OAI.HenonLaneEmden.CapWeights.continuous_profile line 37
7. lemma OAI.HenonLaneEmden.CapWeights.profile_as_div line 41
8. lemma OAI.HenonLaneEmden.CapWeights.profile_center_oscillation line 48
9. lemma OAI.HenonLaneEmden.CapWeights.profile_radial_oscillation line 58
10. lemma OAI.HenonLaneEmden.CapWeights.profile_oscillation line 80
11. def OAI.HenonLaneEmden.CapWeights.normalizer line 89
12. lemma OAI.HenonLaneEmden.CapWeights.integrable_profile line 91
13. lemma OAI.HenonLaneEmden.CapWeights.normalizer_nonneg line 96
14. lemma OAI.HenonLaneEmden.CapWeights.normalizer_bounds line 99
15. lemma OAI.HenonLaneEmden.CapWeights.continuousOn_normalizer line 120
16. def OAI.HenonLaneEmden.CapWeights.normalized line 135

    Source documentation

    Every cap is normalized exactly, with no rotational-invariance assumption.

    def normalized (θ : T) (l : ℝ) (e : T) : ℝ := profile θ l e / normalizer σ θ l
    …

    Mentions: OAI.HenonLaneEmden.CapWeights.profile, OAI.HenonLaneEmden.CapWeights.normalizer

17. lemma OAI.HenonLaneEmden.CapWeights.integral_normalized line 138
18. lemma OAI.HenonLaneEmden.CapWeights.normalized_nonneg line 144
19. lemma OAI.HenonLaneEmden.CapWeights.normalized_le_inv line 148
20. lemma OAI.HenonLaneEmden.CapWeights.normalizer_oscillation line 153
21. lemma OAI.HenonLaneEmden.CapWeights.normalized_oscillation line 182