OAI/Analysis/AffineBernstein/LogTubeMeasure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.measurable_logSpace line 17
2. def OAI.AffineBernstein.logTubeMeasure line 24

   Source comment

   The actual logarithmic pushforward of a tube density, restricted to its positive base domain. Only the nonnegative part outside that domain is discarded.

   def logTubeMeasure (μ : Measure (Space k)) (D : Set (Space k)) (F : Space k × E → ℝ) :
       Measure (Space k) :=
   …

   Mentions: OAI.AffineBernstein.Space

3. lemma OAI.AffineBernstein.logPullback_zero_outside_domain line 30
4. lemma OAI.AffineBernstein.integral_logTubeMeasure line 45
5. lemma OAI.AffineBernstein.integral_logTubeMeasure_mul line 73
6. lemma OAI.AffineBernstein.logPullback_sq line 87
7. lemma OAI.AffineBernstein.logTubeMeasure_compact_lt_top line 92
8. lemma OAI.AffineBernstein.integrable_logTubeMeasure line 125