OAI/Analysis/Mahler/FormLocalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MahlerStokes.extDeriv_finsetSum line 11
2. theorem OAI.MahlerStokes.extDeriv_partition_sum line 21

   Source documentation

   The cutoff derivatives cancel because the actual localized forms sum to ω on a neighborhood; no boundary or Stokes equation is assumed.

   theorem extDeriv_partition_sum {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {n : ℕ} {ι : Type*} [Fintype ι] {W : Set E} {x : E}
       (ρ : ι → E → ℝ) (ω : E → E [⋀^Fin n]→L[ℝ] ℝ)
       (hW : IsOpen W) (hx : x ∈ W) (hsum : ∀ z ∈ W, ∑ i, ρ i z = 1)
       (hω : ∀ i, DifferentiableAt ℝ (fun z => ρ i z • ω z) x) :
       extDeriv ω x = ∑ i, extDeriv (fun z => ρ i z • ω z) x := by
   …

3. theorem OAI.MahlerStokes.contDiff_localized_form line 33
4. theorem OAI.MahlerStokes.hasCompactSupport_localized_form line 40
5. theorem OAI.MahlerStokes.integrable_extDeriv_coefficient line 48

   Source documentation

   Every localized C1 compactly supported form has an integrable actual exterior-derivative coefficient on the whole coordinate space.

   theorem integrable_extDeriv_coefficient {n : ℕ}
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hω : ContDiff ℝ 1 ω) (hc : HasCompactSupport ω) :
       Integrable (fun x => extDeriv ω x (coordinateBasis (n+1))) := by
   …

   Mentions: OAI.MahlerStokes.coordinateBasis

6. theorem OAI.MahlerStokes.integral_extDeriv_partition line 65

   Source documentation

   Actual volume integral localization for a finite smooth partition, on any measurable set contained in its sum-one neighborhood.

   theorem integral_extDeriv_partition {n : ℕ} {ι : Type*} [Fintype ι]
       {K W s : Set (Fin (n+1) → ℝ)}
       (ρ : SmoothPartitionOfUnity ι 𝓘(ℝ, Fin (n+1) → ℝ) (Fin (n+1) → ℝ) K)
       (ω : (Fin (n+1) → ℝ) → (Fin (n+1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
       (hW : IsOpen W) (hsW : s ⊆ W) (hs : MeasurableSet s)
       (hsum : ∀ x ∈ W, ∑ i, ρ i x = 1)
       (hρ : ∀ i, HasCompactSupport (ρ i))
       (hω : ∀ i, ∀ x ∈ tsupport (ρ i), ContDiffAt ℝ 1 ω x) :
       (∫ x in s, extDeriv ω x (coordinateBasis (n+1))) =
         ∑ i, ∫ x in s, extDeriv (fun z => ρ i z • ω z) x (coordinateBasis (n+1)) := by
   …

   Mentions: OAI.MahlerStokes.coordinateBasis