SourceLevelFlux.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.MassHypotheses.contDiffAt_energy line 18
Source documentation
Smoothness of the literal energy, at any finite order, is derived from first-order holomorphicity on the open source domain.
```
theorem MassHypotheses.contDiffAt_energy (h : MassHypotheses n N m U f G)
    {x : ComplexEuclidean n} (hx : x ∈ U) (r : ℕ) :
    ContDiffAt ℝ r (energy f) x := by
…
```
Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.ComplexEuclidean, OAI.Mahler.energy
theorem OAI.Mahler.MassHypotheses.tau_pos line 28
theorem OAI.Mahler.MassHypotheses.contDiffAt_logTau line 35
def OAI.Mahler.sourceBoundaryForm line 44
Source documentation
The finite shuffle form used in both Stokes equations.
```
def sourceBoundaryForm (u : ComplexEuclidean n → ℂ) (k : ℕ) (x : ComplexEuclidean n) :
    ComplexEuclidean n [⋀^Fin 1 ⊕ WedgePowerSlots k]→ₗ[ℝ] ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.WedgePowerSlots

theorem OAI.Mahler.sourceBoundaryForm_level_pullback line 51

Source documentation

Full scaling on any parametrization of a positive level. The tangent condition follows by differentiating its level equation.

theorem sourceBoundaryForm_level_pullback {V : Type*} [NormedAddCommGroup V]
    [NormedSpace ℝ V] {φ : V → ComplexEuclidean n} {y : V} {R : ℝ}
    (h : MassHypotheses n N m U f G) (hR : 0 < R) (hx : φ y ∈ U)
    (hφ : DifferentiableAt ℝ φ y)
    (hlevel : (fun z => tau f (φ z)) =ᶠ[𝓝 y] (fun _ => R)) (k : ℕ) :
    (sourceBoundaryForm (logTau f) k (φ y)).compLinearMap (fderiv ℝ φ y).toLinearMap =
      ((R : ℂ)⁻¹)^(k+1) •
        (sourceBoundaryForm (energy f) k (φ y)).compLinearMap (fderiv ℝ φ y).toLinearMap := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.tau, OAI.Mahler.sourceBoundaryForm, OAI.Mahler.logTau, OAI.Mahler.energy

theorem OAI.Mahler.sourceBoundaryForm_regular_face line 90

Source documentation

Instantiation on the actual regular boundary charts constructed by Stokes.

theorem sourceBoundaryForm_regular_face {d : ℕ}
    (h : MassHypotheses n N m U f G)
    (Ψ : (Fin (d+1) → ℝ) ≃L[ℝ] ComplexEuclidean n)
    (p : MahlerStokes.RegularBoundaryPatch (d+1) (Ψ ⁻¹' U) (fun x => tau f (Ψ x)))
    {R : ℝ} (hR : 0 < R) {y : Fin d → ℝ} (hy : y ∈ p.faceDomain R) (k : ℕ) :
    (sourceBoundaryForm (logTau f) k (Ψ (p.faceParam R y))).compLinearMap
      (fderiv ℝ (fun z => Ψ (p.faceParam R z)) y).toLinearMap =
      ((R : ℂ)⁻¹)^(k+1) •
        (sourceBoundaryForm (energy f) k (Ψ (p.faceParam R y))).compLinearMap
          (fderiv ℝ (fun z => Ψ (p.faceParam R z)) y).toLinearMap := by
…

Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.ComplexEuclidean, OAI.MahlerStokes.RegularBoundaryPatch, OAI.Mahler.tau, OAI.Mahler.sourceBoundaryForm, OAI.Mahler.logTau, OAI.Mahler.energy

theorem OAI.Mahler.complexCoordinates_wedge_basis line 111
Source documentation
The existing Stokes coordinates carry the wedge slots to the exact positive interleaved frame used by the Hessian normalization.
```
theorem complexCoordinates_wedge_basis (s : WedgePowerSlots n) :
    MahlerStokes.complexCoordinates n
      (MahlerStokes.coordinateBasis (n*2) (finProdFinEquiv (pairSlotEquiv n s))) =
      interleavedBasis s := by
…
```
Mentions: OAI.Mahler.WedgePowerSlots, OAI.MahlerStokes.complexCoordinates, OAI.MahlerStokes.coordinateBasis, OAI.Mahler.pairSlotEquiv, OAI.Mahler.interleavedBasis
theorem OAI.Mahler.source_log_top_coefficient_nonneg line 119
Source documentation
Actual logarithmic top-form density is nonnegative in the positive Stokes coordinate frame, with no positivity assumption.
```
theorem source_log_top_coefficient_nonneg (h : MassHypotheses n N m U f G)
    {x : ComplexEuclidean n} (hx : x ∈ U) (hne : x ≠ 0) :
    0 ≤ (wedgePower (extDeriv (oneForm (dcLinear (logTau f))) x).toAlternatingMap n
      (fun s => MahlerStokes.complexCoordinates n
        (MahlerStokes.coordinateBasis (n*2) (finProdFinEquiv (pairSlotEquiv n s))))).re := by
…
```
Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.ComplexEuclidean, OAI.Mahler.wedgePower, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.logTau, OAI.MahlerStokes.complexCoordinates, OAI.MahlerStokes.coordinateBasis, OAI.Mahler.pairSlotEquiv
theorem OAI.Mahler.source_massDensity_coordinate_coefficient line 133
Source documentation
The mass coefficient in Stokes coordinates, with scale one.
```
theorem source_massDensity_coordinate_coefficient (h : MassHypotheses n N m U f G)
    {x : ComplexEuclidean n} (hx : x ∈ U) :
    massDensity f x =
      (wedgePower (extDeriv (oneForm (dcLinear (energy f))) x).toAlternatingMap n
        (fun s => MahlerStokes.complexCoordinates n
          (MahlerStokes.coordinateBasis (n*2) (finProdFinEquiv (pairSlotEquiv n s))))).re := by
…
```
Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.ComplexEuclidean, OAI.Mahler.massDensity, OAI.Mahler.wedgePower, OAI.Mahler.oneForm, OAI.Mahler.dcLinear, OAI.Mahler.energy, OAI.MahlerStokes.complexCoordinates, OAI.MahlerStokes.coordinateBasis, OAI.Mahler.pairSlotEquiv