OAI/Analysis/Mahler/SphereFluxDifferentiation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.continuousOn_orientedDensity line 11
2. lemma OAI.Mahler.hasDerivAt_orientedDensity line 26
3. theorem OAI.Mahler.sphereFlux_continuousOn line 36
4. theorem OAI.Mahler.sphereFlux_continuous line 50
5. theorem OAI.Mahler.sphereFlux_hasDerivAt line 65

   Source documentation

   Differentiation of the actual outward unit-sphere flux. C1 means joint continuity of every form coefficient and its parameter derivative on the compact cylinder; all integral side conditions are derived.

   theorem sphereFlux_hasDerivAt {k : ℕ}
       {B D : ℝ → ComplexEuclidean (k+1) →
         ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ} {a b t : ℝ}
       (hB : ∀ v, ContinuousOn
         (fun p : ℝ × sphere (0 : ComplexEuclidean (k+1)) 1 => B p.1 p.2 v)
         (Icc a b ×ˢ univ))
       (hD : ∀ v, ContinuousOn
         (fun p : ℝ × sphere (0 : ComplexEuclidean (k+1)) 1 => D p.1 p.2 v)
         (Icc a b ×ˢ univ))
       (hd : ∀ s ∈ Ioo a b, ∀ x : sphere (0 : ComplexEuclidean (k+1)) 1, ∀ v,
         HasDerivAt (fun r => B r x v) (D s x v) s)
       (ht : t ∈ Ioo a b) :
   …

   Mentions: OAI.Mahler.ComplexEuclidean

6. theorem OAI.Mahler.sphereFlux_hasDerivAt_of_density line 95

   Source documentation

   A tangent-restricted pointwise calculation can be supplied directly as a density derivative; no ambient extension of that derivative is required.

   theorem sphereFlux_hasDerivAt_of_density {k : ℕ}
       {B D : ℝ → ComplexEuclidean (k+1) →
         ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ} {a b t : ℝ}
       (hB : ∀ v, ContinuousOn
         (fun p : ℝ × sphere (0 : ComplexEuclidean (k+1)) 1 => B p.1 p.2 v)
         (Icc a b ×ˢ univ))
       (hD : ∀ v, ContinuousOn
         (fun p : ℝ × sphere (0 : ComplexEuclidean (k+1)) 1 => D p.1 p.2 v)
         (Icc a b ×ˢ univ))
       (hd : ∀ s ∈ Ioo a b, ∀ x : sphere (0 : ComplexEuclidean (k+1)) 1,
         HasDerivAt (fun r => orientedDensity (sphereFrame k) (sphereVolume k) (B r x) x)
           (orientedDensity (sphereFrame k) (sphereVolume k) (D s x) x) s)
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.orientedDensity, OAI.Mahler.sphereFrame, OAI.Mahler.sphereVolume