OAI/Analysis/Mahler/DimensionTwoAssembly.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.MassHypotheses.source_limit_of_radius_identity line 13

   Source documentation

   Eventual equality suffices for the one-sided limit. The zero and negative-radius branches never enter the statement.

   theorem MassHypotheses.source_limit_of_radius_identity {k N m : ℕ}
       {U : Set (ComplexEuclidean (k+1))} {f : Fin N → ComplexEuclidean (k+1) → ℂ}
       {G : Fin N → MvPolynomial (Fin (k+1)) ℂ} (h : MassHypotheses (k+1) N m U f G)
       (hbridge : (fun r => MahlerStokes.sphereFlux r
         (sourceCoordinateForm (sourceCoordinates k) (logTau f) k)) =ᶠ[𝓝[>] (0:ℝ)]
         (fun r => (radiusSphereFlux k (logTau f) r).re)) :
       Tendsto (fun r => MahlerStokes.sphereFlux r
         (sourceCoordinateForm (sourceCoordinates k) (logTau f) k))
         (𝓝[>] (0:ℝ)) (𝓝 (homogeneousSphereFlux k N G)) :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.MahlerStokes.sphereFlux, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.sourceCoordinates, OAI.Mahler.logTau, OAI.Mahler.radiusSphereFlux, OAI.Mahler.homogeneousSphereFlux

2. theorem OAI.Mahler.MassHypotheses.source_flux_constant_pos line 26

   Source documentation

   The homogeneous flux constant is strictly positive under the degree hypothesis, in every positive complex dimension.

   theorem MassHypotheses.source_flux_constant_pos {k N m : ℕ}
       {U : Set (ComplexEuclidean (k+1))} {f : Fin N → ComplexEuclidean (k+1) → ℂ}
       {G : Fin N → MvPolynomial (Fin (k+1)) ℂ} (h : MassHypotheses (k+1) N m U f G) :
       0 < (Real.pi*(m:ℝ))^(k+1) := by
   …

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

3. theorem OAI.Mahler.MassHypotheses.source_two_numeric_limit_of_radius_identity line 35

   Source documentation

   The dimension-two numerical homogeneous-flux value is determined. The matching coordinate/radius integral identity is an explicit hypothesis.

   theorem MassHypotheses.source_two_numeric_limit_of_radius_identity {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)
       (hbridge : (fun r => MahlerStokes.sphereFlux r
         (sourceCoordinateForm (sourceCoordinates 1) (logTau f) 1)) =ᶠ[𝓝[>] (0:ℝ)]
         (fun r => (radiusSphereFlux 1 (logTau f) r).re)) :
       Tendsto (fun r => MahlerStokes.sphereFlux r
         (sourceCoordinateForm (sourceCoordinates 1) (logTau f) 1))
         (𝓝[>] (0:ℝ)) (𝓝 ((Real.pi*(m:ℝ))^2)) := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.MahlerStokes.sphereFlux, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.sourceCoordinates, OAI.Mahler.logTau, OAI.Mahler.radiusSphereFlux

4. theorem OAI.SymmetricMahler.symmetric_mahler_two_of_source_radius_identity line 53

   Source documentation

   The dimension-two body inequality, conditional on the coordinate/radius flux identity for special maps. The flux identity is retained as a hypothesis.

   theorem symmetric_mahler_two_of_source_radius_identity
       (hbridge : ∀ N (A : Matrix (Fin N) (Fin 2) ℝ),
         Function.Injective (measurement A) → ∀ m : ℕ, 2 ≤ m →
         (fun r => MahlerStokes.sphereFlux r
           (Mahler.sourceCoordinateForm (Mahler.sourceCoordinates 1)
             (Mahler.logTau (euclideanSpecialMap A m)) 1)) =ᶠ[𝓝[>] (0:ℝ)]
           (fun r => (Mahler.radiusSphereFlux 1 (Mahler.logTau (euclideanSpecialMap A m)) r).re))
       {K : Set (Fin 2 → ℝ)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
       8 ≤ (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.Mahler.radiusSphereFlux, OAI.SymmetricMahler.coordinatePolar