OAI/Analysis/Mahler/RegularChartStokes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.setIntegral_extDeriv_congr_support line 11
2. lemma OAI.MahlerStokes.chart_image_target_inter line 30
3. def OAI.MahlerStokes.chartBoundaryFlux line 44

   Source documentation

   Actual oriented boundary-chart integral in the level coordinates.

   def chartBoundaryFlux {n : ℕ}
       (e : OpenPartialHomeomorph (Fin (n+1) → ℝ) (Fin (n+1) → ℝ))
       (k : Fin (n+1)) (R : ℝ)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ) : ℝ :=
   …

4. theorem OAI.MahlerStokes.integral_extDeriv_chart line 53

   Source documentation

   Stokes for a localized form in a genuine boundary chart. All pullback regularity, zero extension, Jacobian and outward signs are derived.

   theorem integral_extDeriv_chart {n : ℕ} {D : Set (Fin (n+1) → ℝ)}
       (e : OpenPartialHomeomorph (Fin (n+1) → ℝ) (Fin (n+1) → ℝ))
       (k : Fin (n+1)) (R : ℝ)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hD : MeasurableSet D) (he : ContDiffOn ℝ 2 e e.source)
       (hi : ContDiffOn ℝ 2 e.symm e.target) (hω : ContDiff ℝ 1 ω)
       (hc : HasCompactSupport ω) (hs : tsupport ω ⊆ e.source)
       (hflat : ∀ x ∈ tsupport ω, x ∈ D ↔ e x k < R) :
       (∫ x in D, extDeriv ω x (coordinateBasis (n+1))) = chartBoundaryFlux e k R ω := by
   …

   Mentions: OAI.MahlerStokes.coordinateBasis, OAI.MahlerStokes.chartBoundaryFlux

5. theorem OAI.MahlerStokes.integral_extDeriv_regular_partition line 106

   Source documentation

   Stokes with a fixed admissible atlas and partition. The same boundary representation can therefore be used for two different forms.

   theorem integral_extDeriv_regular_partition {n : ℕ} {U : Set (Fin (n+1) → ℝ)}
       {g : (Fin (n+1) → ℝ) → ℝ} {R : ℝ}
       (hU : IsOpen U) (hg : ContinuousOn g U)
       (a : RegularBoundaryAtlas (n+1) U g (frontier (regularSublevel U g R)))
       {W : Set (Fin (n+1) → ℝ)}
       (ρ : SmoothPartitionOfUnity (Option a.Index) 𝓘(ℝ, Fin (n+1) → ℝ)
         (Fin (n+1) → ℝ) (closure W))
       (hWo : IsOpen W) (hCW : closure (regularSublevel U g R) ⊆ W)
       (hρc : ∀ i, HasCompactSupport (ρ i)) (hρsub : ρ.IsSubordinate (sublevelPatchDomain a))
       (hsum : ∀ x ∈ W, ∑ i, ρ i x = 1)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 1 ω U) :
   …

   Mentions: OAI.MahlerStokes.RegularBoundaryAtlas, OAI.MahlerStokes.regularSublevel, OAI.MahlerStokes.sublevelPatchDomain

6. theorem OAI.MahlerStokes.exists_regular_sublevel_stokes line 146

   Source documentation

   General regular-sublevel Stokes for actual C1 differential forms. Compactness supplies the finite charts and smooth cutoffs, whose oriented boundary integrals are assembled here.

   theorem exists_regular_sublevel_stokes {n : ℕ} {U : Set (Fin (n+1) → ℝ)}
       {g : (Fin (n+1) → ℝ) → ℝ} {R : ℝ}
       (hU : IsOpen U) (hg : ContDiffOn ℝ 2 g U)
       (hc : IsCompact (closure (regularSublevel U g R)))
       (hcl : closure (regularSublevel U g R) ⊆ U)
       (hreg : ∀ x ∈ U, g x = R → fderiv ℝ g x ≠ 0)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiffOn ℝ 1 ω U) :
       ∃ (a : RegularBoundaryAtlas (n+1) U g (frontier (regularSublevel U g R)))
         (W : Set (Fin (n+1) → ℝ))
         (ρ : SmoothPartitionOfUnity (Option a.Index) 𝓘(ℝ, Fin (n+1) → ℝ)
           (Fin (n+1) → ℝ) (closure W)),
   …

   Mentions: OAI.MahlerStokes.regularSublevel, OAI.MahlerStokes.RegularBoundaryAtlas