OAI/Analysis/AffineBernstein/TubeCombination.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.tubeBasePair_linearCombination line 17
2. def OAI.AffineBernstein.positiveOrthant line 42

   Source comment

   The manuscript's positive base orthant.

   def positiveOrthant (k : ℕ) : Set (Space k) := {s | ∀ i, 0 < s i}

   Mentions: OAI.AffineBernstein.Space

3. def OAI.AffineBernstein.logSpace line 44
4. def OAI.AffineBernstein.expSpace line 47
5. lemma OAI.AffineBernstein.logSpace_apply line 50
6. lemma OAI.AffineBernstein.expSpace_apply line 51
7. lemma OAI.AffineBernstein.isOpen_positiveOrthant line 53
8. lemma OAI.AffineBernstein.expSpace_mem_positive line 58
9. lemma OAI.AffineBernstein.logSpace_expSpace line 61
10. lemma OAI.AffineBernstein.expSpace_logSpace line 65
11. lemma OAI.AffineBernstein.contDiff_expSpace line 70
12. lemma OAI.AffineBernstein.contDiffAt_logSpace line 74
13. def OAI.AffineBernstein.logPullback line 81

    Source comment

    Extension by zero of a compact test in logarithmic coordinates; a negative coordinate must not be silently sent through Real.log.

    def logPullback {k : ℕ} (φ : Space k → ℝ) (s : Space k) : ℝ :=
    …

    Mentions: OAI.AffineBernstein.Space

14. lemma OAI.AffineBernstein.logPullback_of_positive line 84
15. lemma OAI.AffineBernstein.logPullback_eventuallyEq line 87
16. lemma OAI.AffineBernstein.support_logPullback_subset line 92
17. lemma OAI.AffineBernstein.tsupport_logPullback_subset line 103
18. lemma OAI.AffineBernstein.hasCompactSupport_logPullback line 107
19. lemma OAI.AffineBernstein.contDiff_logPullback line 112
20. lemma OAI.AffineBernstein.tsupport_logPullback_subset_logDomain line 128