SphereDensityBridge.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Mahler.restMap line 17
lemma OAI.Mahler.restMap_spec line 26
lemma OAI.Mahler.perm_fixed_first_mem line 38

lemma OAI.Mahler.wedge_one_outward line 65

Source documentation

The shuffle product has coefficient one on an outward normal followed by tangent vectors. This includes its normalization, in arbitrary degree.

lemma wedge_one_outward {T κ : Type*} [AddCommGroup T] [Module ℝ T]
    [Fintype κ] [DecidableEq κ]
    (a : T [⋀^Fin 1]→ₗ[ℝ] ℂ) (B : T [⋀^κ]→ₗ[ℝ] ℂ)
    (x : T) (v : κ → T) (hx : a (fun _ => x) = 1)
    (hv : ∀ j, a (fun _ => v j) = 0) :
    wedge a B (Sum.elim (fun _ => x) v) = B v := by
…

Mentions: OAI.Mahler.wedge

def OAI.Mahler.densityBridgeSlots line 101
Source documentation
Ordered identification of the normal slot and recursive boundary slots.
```
def densityBridgeSlots (k : ℕ) :
    (Fin 1 ⊕ (Fin 1 ⊕ WedgePowerSlots k)) ≃ Fin ((2*k+1)+1) :=
…
```
Mentions: OAI.Mahler.WedgePowerSlots
lemma OAI.Mahler.densityBridgeSlots_normal line 105
lemma OAI.Mahler.densityBridgeSlots_tangent line 109
lemma OAI.Mahler.densityBridgeSlots_frame line 118
lemma OAI.Mahler.densityBridgeSlots_cons line 123
theorem OAI.Mahler.sphereDensity_eq_orientedDensity line 134
Source documentation
The recursive shuffle density is the normalized outward cofactor coefficient. The slot equivalence preserves its positive orientation.
```
theorem sphereDensity_eq_orientedDensity {k : ℕ} {x : ComplexEuclidean (k+1)}
    (hx : ‖x‖ = 1)
    (B : ComplexEuclidean (k+1) [⋀^Fin 1 ⊕ WedgePowerSlots k]→ₗ[ℝ] ℂ) :
    sphereDensity k x B = orientedDensity (sphereFrame k) (sphereVolume k)
      (B.domDomCongr (boundaryFinEquiv k)) x := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.WedgePowerSlots, OAI.Mahler.sphereDensity, OAI.Mahler.orientedDensity, OAI.Mahler.sphereFrame, OAI.Mahler.sphereVolume, OAI.Mahler.boundaryFinEquiv
theorem OAI.Mahler.sphereFlux_eq_integral_sphereDensity line 170
Source documentation
The area integrals agree pointwise for an arbitrary boundary form field. No integrability hypothesis is needed for this real-valued identity.
```
theorem sphereFlux_eq_integral_sphereDensity (k : ℕ)
    (B : ComplexEuclidean (k+1) →
      ComplexEuclidean (k+1) [⋀^Fin 1 ⊕ WedgePowerSlots k]→ₗ[ℝ] ℂ) :
    sphereFlux k (fun x => (B x).domDomCongr (boundaryFinEquiv k)) =
      ∫ z : sphere (0 : ComplexEuclidean (k+1)) 1,
        (sphereDensity k z (B z)).re ∂sphereArea (k+1) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.WedgePowerSlots, OAI.Mahler.sphereFlux, OAI.Mahler.boundaryFinEquiv, OAI.Mahler.sphereDensity, OAI.Mahler.sphereArea

lemma OAI.Mahler.integrable_sphereBoundaryDensity line 183

Source documentation

The actual boundary density is integrable: C2 regularity and compactness supply this premise, rather than assuming an integral exists.

lemma integrable_sphereBoundaryDensity {k : ℕ} {u : ComplexEuclidean (k+1) → ℂ}
    (hu : ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContDiffAt ℝ 2 u (z : ComplexEuclidean (k+1))) :
    Integrable (fun z : sphere (0 : ComplexEuclidean (k+1)) 1 =>
      sphereDensity k z (boundaryForm u k z)) (sphereArea (k+1)) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.sphereDensity, OAI.Mahler.boundaryForm, OAI.Mahler.sphereArea

theorem OAI.Mahler.unitSphereFlux_re_eq_sphereFlux line 198
Source documentation
The complex flux used for the rescaling limit and the real cofactor flux used for homogeneous deformation have exactly the same real part.
```
theorem unitSphereFlux_re_eq_sphereFlux {k : ℕ} {u : ComplexEuclidean (k+1) → ℂ}
    (hu : ∀ z : sphere (0 : ComplexEuclidean (k+1)) 1,
      ContDiffAt ℝ 2 u (z : ComplexEuclidean (k+1))) :
    (unitSphereFlux k u).re = sphereFlux k (boundaryFormFin (dcLinear u)) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.unitSphereFlux, OAI.Mahler.sphereFlux, OAI.Mahler.boundaryFormFin, OAI.Mahler.dcLinear
theorem OAI.Mahler.MassHypotheses.unitSphereFlux_re_eq_homogeneousSphereFlux line 213
Source documentation
For the homogeneous polynomial, the endpoint equality requires only the mass hypotheses.
```
theorem MassHypotheses.unitSphereFlux_re_eq_homogeneousSphereFlux {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) :
    (unitSphereFlux k (logTau (polynomialMap G))).re = homogeneousSphereFlux k N G := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.unitSphereFlux, OAI.Mahler.logTau, OAI.Mahler.polynomialMap, OAI.Mahler.homogeneousSphereFlux

theorem OAI.Mahler.MassHypotheses.small_sphere_real_flux_limit line 229

Source documentation

The varying-radius surface integrals converge to the actual homogeneous cofactor endpoint. No unproved homogeneous-flux constancy is used here.

theorem MassHypotheses.small_sphere_real_flux_limit {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) :
    Filter.Tendsto (fun r => (radiusSphereFlux k (logTau f) r).re)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds (homogeneousSphereFlux k N G)) := by
…

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