OAI/Analysis/Mahler/HemisphereChart.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MahlerStokes.radiusSq_smul line 13
2. lemma OAI.MahlerStokes.chord_pos line 17
3. lemma OAI.MahlerStokes.chord_sq line 20
4. def OAI.MahlerStokes.hemisphereGraph line 28

   Source documentation

   Upper hemisphere graph, in the precise coordinate order used by Stokes.

   def hemisphereGraph {n : ℕ} (i : Fin (n+1)) (y : Fin n → ℝ) : Fin (n+1) → ℝ :=
   …

5. lemma OAI.MahlerStokes.radiusSq_hemisphereGraph line 31
6. def OAI.MahlerStokes.hemisphereCone line 38

   Source documentation

   Radial coordinates on the open upper half-ball. The i-th domain coordinate is radius; all remaining coordinates parametrize the hemisphere.

   def hemisphereCone {n : ℕ} (i : Fin (n+1)) (x : Fin (n+1) → ℝ) : Fin (n+1) → ℝ :=
   …

7. def OAI.MahlerStokes.hemisphereConeDomain line 41
8. lemma OAI.MahlerStokes.radiusSq_hemisphereCone line 44
9. lemma OAI.MahlerStokes.hemisphereCone_injOn line 48
10. lemma OAI.MahlerStokes.hemisphereCone_image line 65
11. def OAI.MahlerStokes.coordinateDot line 114

    Source documentation

    Real dot product as a continuous linear functional on coordinate space.

    def coordinateDot {n : ℕ} (y : Fin n → ℝ) : (Fin n → ℝ) →L[ℝ] ℝ :=
    …

12. lemma OAI.MahlerStokes.coordinateDot_apply line 117
13. lemma OAI.MahlerStokes.hasFDerivAt_radiusSq line 121
14. def OAI.MahlerStokes.chordDerivative line 132
15. lemma OAI.MahlerStokes.hasFDerivAt_chord line 135
16. def OAI.MahlerStokes.hemisphereGraphDerivative line 144

    Source documentation

    Derivative of the hemisphere graph.

    def hemisphereGraphDerivative {n : ℕ} (i : Fin (n+1)) (y : Fin n → ℝ) :
        (Fin n → ℝ) →L[ℝ] (Fin (n+1) → ℝ) :=
    …

17. lemma OAI.MahlerStokes.hasFDerivAt_hemisphereGraph line 148
18. def OAI.MahlerStokes.removeCoordinate line 159
19. def OAI.MahlerStokes.hemisphereConeDerivative line 163
20. lemma OAI.MahlerStokes.hasFDerivAt_hemisphereCone line 168