OAI/Analysis/Mahler/SphereFluxLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.actualRealComplexJet line 10
2. theorem OAI.Mahler.sphereDensity_tendstoUniformlyOn line 17

   Source documentation

   Uniform first and second derivative convergence gives uniform convergence of the actual outward sphere densities. The nonlinear operation is a continuous finite shuffle polynomial.

   theorem sphereDensity_tendstoUniformlyOn {k : ℕ} {I : Type*} {l : Filter I}
       {u : I → ComplexEuclidean (k+1) → ℂ} {v : ComplexEuclidean (k+1) → ℂ}
       {K : Set (ComplexEuclidean (k+1))} (hK : IsCompact K)
       (hv : ContinuousOn (actualRealComplexJet v) K)
       (h1 : TendstoUniformlyOn (fun i => fderiv ℝ (u i)) (fderiv ℝ v) l K)
       (h2 : TendstoUniformlyOn (fun i => fderiv ℝ (fderiv ℝ (u i)))
         (fderiv ℝ (fderiv ℝ v)) l K) :
       TendstoUniformlyOn
         (fun i x => sphereJetDensity k (x, actualRealComplexJet (u i) x))
         (fun x => sphereJetDensity k (x, actualRealComplexJet v x)) l K := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.actualRealComplexJet, OAI.Mahler.sphereJetDensity

3. theorem OAI.Mahler.sphereJetIntegral_tendsto line 40

   Source documentation

   A genuine area integral limit; continuity gives measurability, compactness gives a bounded limit density, and uniform convergence supplies a common integrable constant bound. No integral convergence is a hypothesis.

   theorem sphereJetIntegral_tendsto {k : ℕ} {I : Type*} {l : Filter I}
       [l.IsCountablyGenerated]
       {u : I → ComplexEuclidean (k+1) → ℂ} {v : ComplexEuclidean (k+1) → ℂ}
       {K : Set (ComplexEuclidean (k+1))} (hK : IsCompact K)
       (hS : sphere (0 : ComplexEuclidean (k+1)) 1 ⊆ K)
       (hv : ContinuousOn (actualRealComplexJet v) K)
       (hu : ∀ᶠ i in l, ContinuousOn (actualRealComplexJet (u i)) K)
       (h1 : TendstoUniformlyOn (fun i => fderiv ℝ (u i)) (fderiv ℝ v) l K)
       (h2 : TendstoUniformlyOn (fun i => fderiv ℝ (fderiv ℝ (u i)))
         (fderiv ℝ (fderiv ℝ v)) l K) :
       Tendsto (fun i => ∫ z : sphere (0 : ComplexEuclidean (k+1)) 1,
         sphereJetDensity k ((z : ComplexEuclidean (k+1)), actualRealComplexJet (u i) z)
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.actualRealComplexJet, OAI.Mahler.sphereJetDensity

4. theorem OAI.Mahler.unitSphereFlux_tendsto line 86

   Source documentation

   The limit for actual d^c u wedge (dd^c u)^k, not a surrogate jet integral.

   theorem unitSphereFlux_tendsto {k : ℕ} {I : Type*} {l : Filter I}
       [l.IsCountablyGenerated]
       {u : I → ComplexEuclidean (k+1) → ℂ} {v : ComplexEuclidean (k+1) → ℂ}
       {K : Set (ComplexEuclidean (k+1))} (hK : IsCompact K)
       (hS : sphere (0 : ComplexEuclidean (k+1)) 1 ⊆ K)
       (hv : ContinuousOn (actualRealComplexJet v) K)
       (hu : ∀ᶠ i in l, ContinuousOn (actualRealComplexJet (u i)) K)
       (hdv : ∀ x ∈ K, DifferentiableAt ℝ (fderiv ℝ v) x)
       (hdu : ∀ᶠ i in l, ∀ x ∈ K, DifferentiableAt ℝ (fderiv ℝ (u i)) x)
       (h1 : TendstoUniformlyOn (fun i => fderiv ℝ (u i)) (fderiv ℝ v) l K)
       (h2 : TendstoUniformlyOn (fun i => fderiv ℝ (fderiv ℝ (u i)))
         (fderiv ℝ (fderiv ℝ v)) l K) :
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.actualRealComplexJet