SourceStokes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.MassHypotheses.contDiffAt_tau line 13
theorem OAI.Mahler.MassHypotheses.contDiffOn_coordinateTau line 20
lemma OAI.Mahler.source_sublevel_preimage line 26
theorem OAI.Mahler.MassHypotheses.coordinate_compact_sublevels line 30
theorem OAI.Mahler.MassHypotheses.coordinate_regular line 42

theorem OAI.Mahler.exists_source_stokes_partition line 60

Source documentation

A single regular-level atlas and partition yield Stokes identities for both coordinate forms. The punctured identity holds for every admissible inner radius with that same outer representation. No differential identity or positivity is a premise. Identification of the integrands with top wedge powers is not asserted here.

theorem exists_source_stokes_partition (h : MassHypotheses n N m U f G) (k : ℕ)
    (Ψ : (Fin ((2*k+1)+1) → ℝ) ≃L[ℝ] ComplexEuclidean n)
    {R : ℝ} (hR : 0 < R) (hR1 : R < 1)
    (hreg : ∀ x ∈ U, tau f x = R → fderiv ℝ (tau f) x ≠ 0) :
    ∃ (a : RegularBoundaryAtlas ((2*k+1)+1) (Ψ ⁻¹' U) (fun x => tau f (Ψ x))
        (frontier (regularSublevel (Ψ ⁻¹' U) (fun x => tau f (Ψ x)) R)))
      (W : Set (Fin ((2*k+1)+1) → ℝ))
      (ρ : SmoothPartitionOfUnity (Option a.Index) 𝓘(ℝ, Fin ((2*k+1)+1) → ℝ)
        (Fin ((2*k+1)+1) → ℝ) (closure W)),
      IsOpen W ∧ closure (regularSublevel (Ψ ⁻¹' U) (fun x => tau f (Ψ x)) R) ⊆ W ∧
      (∀ i, HasCompactSupport (ρ i)) ∧ ρ.IsSubordinate (sublevelPatchDomain a) ∧
      (∀ x ∈ W, ∑ i, ρ i x = 1) ∧
…

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