SpecialSourceMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.euclideanSpecial_positive_regular_nonzero line 13

Source documentation

The Stokes regularity condition holds for every positive level of the finite-strip special map.

theorem euclideanSpecial_positive_regular_nonzero {n N m : ℕ}
    (A : Matrix (Fin N) (Fin n) ℝ) (hA : Function.Injective (measurement A))
    (hm : 0 < m) {R : ℝ} (hR : 0 < R)
    {z : Mahler.ComplexEuclidean n} (hz : z ∈ euclideanStripDomain A)
    (hlevel : Mahler.tau (euclideanSpecialMap A m) z = R) :
    fderiv ℝ (Mahler.tau (euclideanSpecialMap A m)) z ≠ 0 := by
…

Mentions: OAI.SymmetricMahler.measurement, OAI.Mahler.ComplexEuclidean, OAI.SymmetricMahler.euclideanStripDomain, OAI.Mahler.tau, OAI.SymmetricMahler.euclideanSpecialMap

theorem OAI.SymmetricMahler.special_regular_mass_of_source_flux_limit line 24

theorem OAI.SymmetricMahler.symmetric_mahler_from_special_source_flux_limits line 42

Source documentation

The arbitrary-body inequality conditional on the numerical coordinate small-sphere limit. The general-dimensional homogeneous flux value is retained as a hypothesis.

theorem symmetric_mahler_from_special_source_flux_limits (n : ℕ)
    (hlimit : ∀ N (A : Matrix (Fin N) (Fin (n+1)) ℝ),
      Function.Injective (measurement A) → ∀ m : ℕ, 2 ≤ m → Tendsto
      (fun r => MahlerStokes.sphereFlux r
        (Mahler.sourceCoordinateForm (Mahler.sourceCoordinates n)
          (Mahler.logTau (euclideanSpecialMap A m)) n))
      (𝓝[>] (0:ℝ)) (𝓝 ((Real.pi*(m:ℝ))^(n+1))))
    {K : Set (Fin (n+1) → ℝ)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
    (4:ℝ)^(n+1)/(Nat.factorial (n+1):ℝ) ≤
      (volume K).toReal*(volume (coordinatePolar K)).toReal := by
…

Mentions: OAI.SymmetricMahler.measurement, OAI.MahlerStokes.sphereFlux, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.sourceCoordinates, OAI.Mahler.logTau, OAI.SymmetricMahler.euclideanSpecialMap, OAI.SymmetricMahler.coordinatePolar