OAI/Analysis/Mahler/HemisphereFlux.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.integral_upperHemisphere line 12

   Source documentation

   The positive normal coordinate cancels the reciprocal-chord surface Jacobian, giving exactly the coordinate hemisphere integral used by Stokes.

   theorem integral_upperHemisphere {n : ℕ} (i : Fin (n+1))
       (f : EuclideanSpace ℝ (Fin (n+1)) → ℝ) :
       (∫ z in range (hemisphereParam i),
         (z : EuclideanSpace ℝ (Fin (n+1))) i * f z
         ∂(volume : Measure (EuclideanSpace ℝ (Fin (n+1)))).toSphere) =
       ∫ y in coordBall n 1, f (toLp 2 (hemisphereGraph i y)) := by
   …

   Mentions: OAI.MahlerStokes.hemisphereParam, OAI.MahlerStokes.coordBall, OAI.MahlerStokes.hemisphereGraph

2. lemma OAI.MahlerStokes.coordBall_neg_preimage line 36
3. lemma OAI.MahlerStokes.neg_hemisphereGraph line 41
4. theorem OAI.MahlerStokes.integral_lowerHemisphere line 51

   Source documentation

   Lower hemisphere, with the negative normal coordinate and the same positive coordinate measure on the parameter ball.

   theorem integral_lowerHemisphere {n : ℕ} (i : Fin (n+1))
       (f : EuclideanSpace ℝ (Fin (n+1)) → ℝ) :
       (∫ z in {z : sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1 |
           (z : EuclideanSpace ℝ (Fin (n+1))) i < 0},
         (z : EuclideanSpace ℝ (Fin (n+1))) i * f z
         ∂(volume : Measure (EuclideanSpace ℝ (Fin (n+1)))).toSphere) =
       -(∫ y in coordBall n 1, f (toLp 2 (i.insertNth (-chord 1 y) y))) := by
   …

   Mentions: OAI.MahlerStokes.coordBall, OAI.MahlerStokes.chord

5. lemma OAI.MahlerStokes.integral_sphere_coordinate_of_integrable line 95
6. lemma OAI.MahlerStokes.mem_unitSphere_of_radiusSq line 130
7. theorem OAI.MahlerStokes.integral_sphere_coordinate line 138

   Source documentation

   Continuity only on the sphere supplies every integrability premise. The integrand may be singular at the origin.

   theorem integral_sphere_coordinate {n : ℕ} (i : Fin (n+1))
       (f : EuclideanSpace ℝ (Fin (n+1)) → ℝ)
       (hf : ContinuousOn f (sphere 0 1)) :
       (∫ z : sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1,
         (z : EuclideanSpace ℝ (Fin (n+1))) i * f z
         ∂(volume : Measure (EuclideanSpace ℝ (Fin (n+1)))).toSphere) =
       ∫ y in coordBall n 1,
         f (toLp 2 (i.insertNth (chord 1 y) y)) - f (toLp 2 (i.insertNth (-chord 1 y) y)) := by
   …

   Mentions: OAI.MahlerStokes.coordBall, OAI.MahlerStokes.chord