OAI/Analysis/Mahler/HomogeneousTwoFlux.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.MassHypotheses.homogeneousTwoPrimitive_C2 line 13
2. theorem OAI.Mahler.MassHypotheses.homogeneousTwoPrimitive_flux_zero line 23

   Source documentation

   The closed-sphere integral of the dimension-two primitive vanishes. C2 follows from the mass hypotheses; it is not an added premise.

   theorem MassHypotheses.homogeneousTwoPrimitive_flux_zero {N m : ℕ}
       {U : Set (ComplexEuclidean 2)} {f : Fin N → ComplexEuclidean 2 → ℂ}
       {G : Fin N → MvPolynomial (Fin 2) ℂ} (h : MassHypotheses 2 N m U f G) (t : ℝ) :
       sphereFlux 1 (fun x => (extDeriv (homogeneousTwoPrimitive (m := m) G t) x).toAlternatingMap) = 0 := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.sphereFlux, OAI.Mahler.homogeneousTwoPrimitive

3. theorem OAI.Mahler.MassHypotheses.homogeneousResidualFlux_two_eq_zero line 34
4. theorem OAI.Mahler.MassHypotheses.homogeneousPathFlux_two_constant line 64

   Source documentation

   The actual homogeneous flux is constant on the whole parameter line in complex dimension two. No integral identity remains as a premise.

   theorem MassHypotheses.homogeneousPathFlux_two_constant {N m : ℕ}
       {U : Set (ComplexEuclidean 2)} {f : Fin N → ComplexEuclidean 2 → ℂ}
       {G : Fin N → MvPolynomial (Fin 2) ℂ} (h : MassHypotheses 2 N m U f G) (a b : ℝ) :
       homogeneousPathFlux 1 N m G b = homogeneousPathFlux 1 N m G a := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousPathFlux

5. theorem OAI.Mahler.MassHypotheses.homogeneousSphereFlux_two_value line 73

   Source documentation

   The homogeneous unit-sphere value in complex dimension two.

   theorem MassHypotheses.homogeneousSphereFlux_two_value {N m : ℕ}
       {U : Set (ComplexEuclidean 2)} {f : Fin N → ComplexEuclidean 2 → ℂ}
       {G : Fin N → MvPolynomial (Fin 2) ℂ} (h : MassHypotheses 2 N m U f G) :
       homogeneousSphereFlux 1 N G = (Real.pi * (m : ℝ))^2 := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousSphereFlux

6. theorem OAI.Mahler.MassHypotheses.small_sphere_real_flux_limit_two line 82

   Source documentation

   The radius-sphere flux limit in complex dimension two, from MassHypotheses alone.

   theorem MassHypotheses.small_sphere_real_flux_limit_two {N m : ℕ}
       {U : Set (ComplexEuclidean 2)} {f : Fin N → ComplexEuclidean 2 → ℂ}
       {G : Fin N → MvPolynomial (Fin 2) ℂ} (h : MassHypotheses 2 N m U f G) :
       Filter.Tendsto (fun r => (radiusSphereFlux 1 (logTau f) r).re)
         (nhdsWithin 0 (Ioi 0)) (nhds ((Real.pi * (m : ℝ))^2)) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.radiusSphereFlux, OAI.Mahler.logTau