OAI/Topology/EilenbergGanea/IntegralDegree.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EilenbergGanea.compact_selected_fiber line 24
2. theorem OAI.EilenbergGanea.exists_constant_jacobian_sign_patch line 41

   Source comment

   The determinant retains its sign on a sufficiently small neighborhood of a regular point.

   theorem exists_constant_jacobian_sign_patch (f : E → E) {x : E}
       (hf : ContDiff ℝ 1 f) (hd : (fderiv ℝ f x).det ≠ 0) (W : Set E)
       (hW : IsOpen W) (hxW : x ∈ W) :
       ∃ V : Set E, IsOpen V ∧ x ∈ V ∧ V ⊆ W ∧ InjOn f V ∧ IsOpen (f '' V) ∧
         ∀ z ∈ V, (fderiv ℝ f z).det =
           (if 0 < (fderiv ℝ f x).det then 1 else -1) * |(fderiv ℝ f z).det| := by
   …

3. theorem OAI.EilenbergGanea.disjoint_regular_inverse_patches line 82

   Source comment

   Finitely many regular roots admit pairwise disjoint inverse neighborhoods, all contained in the prescribed isolating open set.

   theorem disjoint_regular_inverse_patches (f : E → E) (hf : ContDiff ℝ 1 f)
       (U : Set E) (hU : IsOpen U) (S : Set E) (hS : S.Finite)
       (hSU : S ⊆ U) (hd : ∀ x ∈ S, (fderiv ℝ f x).det ≠ 0) :
       ∃ V : S → Set E,
         (∀ x, IsOpen (V x) ∧ (x : E) ∈ V x ∧ V x ⊆ U ∧ InjOn f (V x) ∧
           IsOpen (f '' V x) ∧ ∀ z ∈ V x, (fderiv ℝ f z).det =
             (if 0 < (fderiv ℝ f x).det then 1 else -1) * |(fderiv ℝ f z).det|) ∧
         Pairwise (fun x y => Disjoint (V x) (V y)) := by
   …

4. theorem OAI.EilenbergGanea.exists_target_neighborhood_of_patches line 105
5. def OAI.EilenbergGanea.jacobianIntegral line 146

   Source comment

   The integral representative of local degree against a target bump.

   def jacobianIntegral (f : E → E) (U : Set E) (ρ : E → ℝ) : ℝ :=
   …

6. theorem OAI.EilenbergGanea.jacobianIntegral_of_injOn line 150

   Source comment

   The signed change-of-variables formula on one regular inverse patch.

   theorem jacobianIntegral_of_injOn (f : E → E) (U : Set E) (hU : MeasurableSet U)
       (hf : ∀ x ∈ U, DifferentiableAt ℝ f x) (hinj : InjOn f U)
       (ρ : E → ℝ) (σ : ℝ) (hσ : ∀ x ∈ U,
         (fderiv ℝ f x).det = σ * |(fderiv ℝ f x).det|) :
       jacobianIntegral μ f U ρ = σ * ∫ y in f '' U, ρ y ∂μ := by
   …

   Mentions: OAI.EilenbergGanea.jacobianIntegral

7. theorem OAI.EilenbergGanea.jacobianIntegral_inverse_patch line 167

   Source comment

   If the normalized target bump is supported inside an inverse patch, the patch contributes exactly the sign of its Jacobian.

   theorem jacobianIntegral_inverse_patch (f : E → E) (U : Set E) (hU : MeasurableSet U)
       (hf : ∀ x ∈ U, DifferentiableAt ℝ f x) (hinj : InjOn f U)
       (ρ : E → ℝ) (σ : ℝ) (hσ : ∀ x ∈ U,
         (fderiv ℝ f x).det = σ * |(fderiv ℝ f x).det|)
       (hsupp : Function.support ρ ⊆ f '' U) (hunit : ∫ y, ρ y ∂μ = 1) :
       jacobianIntegral μ f U ρ = σ := by
   …

   Mentions: OAI.EilenbergGanea.jacobianIntegral

8. theorem OAI.EilenbergGanea.jacobianIntegral_sum_patches line 183
9. theorem OAI.EilenbergGanea.jacobianIntegral_eq_sum_signs line 203

   Source comment

   The regular signed-count formula, once disjoint inverse patches and a small normalized target bump have been chosen.

   theorem jacobianIntegral_eq_sum_signs {ι : Type*} [Fintype ι]
       (f : E → E) (U : Set E) (hU : MeasurableSet U) (V : ι → Set E)
       (hV : ∀ i, MeasurableSet (V i)) (hsub : ∀ i, V i ⊆ U)
       (hdisj : Pairwise (fun i j => Disjoint (V i) (V j)))
       (hf : ∀ x ∈ U, DifferentiableAt ℝ f x) (hinj : ∀ i, InjOn f (V i))
       (ρ : E → ℝ) (σ : ι → ℝ)
       (hσ : ∀ i x, x ∈ V i → (fderiv ℝ f x).det = σ i * |(fderiv ℝ f x).det|)
       (hcovered : ∀ x ∈ U, ρ (f x) ≠ 0 → ∃ i, x ∈ V i)
       (hsupp : ∀ i, Function.support ρ ⊆ f '' V i)
       (hunit : ∫ y, ρ y ∂μ = 1)
       (hint : IntegrableOn (fun x => (fderiv ℝ f x).det * ρ (f x)) U μ) :
       jacobianIntegral μ f U ρ = ∑ i, σ i := by
   …

   Mentions: OAI.EilenbergGanea.jacobianIntegral

10. theorem OAI.EilenbergGanea.jacobianIntegral_eq_zero_of_no_preimage line 224
11. theorem OAI.EilenbergGanea.exists_normalized_smooth_bump line 241

    Source documentation

    A normalized smooth target bump can be supported in any prescribed neighborhood of the target.

    theorem exists_normalized_smooth_bump (y : E) (N : Set E) (hN : IsOpen N) (hy : y ∈ N) :
        ∃ ρ : E → ℝ, ContDiff ℝ ∞ ρ ∧ HasCompactSupport ρ ∧ tsupport ρ ⊆ N ∧
          (∫ z, ρ z ∂μ) = 1 := by
    …

12. theorem OAI.EilenbergGanea.regular_signed_count_neighborhood line 255

    Source documentation

    One target neighborhood works for every normalized continuous density. This uniformity lets the same density be used throughout a localized homotopy.

    theorem regular_signed_count_neighborhood (f : E → E) (hf : ContDiff ℝ 1 f)
        (y : E) (U : Set E) (hU : IsOpen U) (hc : IsCompact (closure U))
        (hb : ∀ x ∈ frontier U, f x ≠ y) (s : Finset E)
        (hs : ∀ x, x ∈ s ↔ x ∈ U ∧ f x = y)
        (hd : ∀ x ∈ s, (fderiv ℝ f x).det ≠ 0) :
        ∃ N : Set E, IsOpen N ∧ y ∈ N ∧ ∀ ρ : E → ℝ, Continuous ρ →
          Function.support ρ ⊆ N → (∫ z, ρ z ∂μ) = 1 →
          jacobianIntegral μ f U ρ = ∑ x ∈ s, (if 0 < (fderiv ℝ f x).det then 1 else -1) := by
    …

    Mentions: OAI.EilenbergGanea.jacobianIntegral

13. theorem OAI.EilenbergGanea.regular_signed_count_density line 289

    Source documentation

    The analytic representative has exactly the expected signed regular count for a sufficiently concentrated normalized target bump.

    theorem regular_signed_count_density (f : E → E) (hf : ContDiff ℝ 1 f)
        (y : E) (U : Set E) (hU : IsOpen U) (hc : IsCompact (closure U))
        (hb : ∀ x ∈ frontier U, f x ≠ y) (s : Finset E)
        (hs : ∀ x, x ∈ s ↔ x ∈ U ∧ f x = y)
        (hd : ∀ x ∈ s, (fderiv ℝ f x).det ≠ 0) :
        ∃ ρ : E → ℝ, ContDiff ℝ ∞ ρ ∧ HasCompactSupport ρ ∧ (∫ z, ρ z ∂μ) = 1 ∧
          jacobianIntegral μ f U ρ = ∑ x ∈ s, (if 0 < (fderiv ℝ f x).det then 1 else -1) := by
    …

    Mentions: OAI.EilenbergGanea.jacobianIntegral

14. def OAI.EilenbergGanea.coordinateBasis line 327

    Source documentation

    Standard coordinate basis as a tuple of vectors.

    def coordinateBasis (n : ℕ) : Fin n → (Fin n → ℝ) := fun i => Pi.single i 1

15. def OAI.EilenbergGanea.formFlux line 330

    Source documentation

    The signed coordinate coefficient of an n-form in dimension n+1.

    def formFlux {n : ℕ} (form : (Fin (n + 1) → ℝ) →
        (Fin (n + 1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ) (i : Fin (n + 1))
        (x : Fin (n + 1) → ℝ) : ℝ :=
    …

16. theorem OAI.EilenbergGanea.integral_extDeriv_box line 338

    Source documentation

    Stokes on a rectangular box, as a direct consequence of Mathlib's Bochner divergence theorem. No smoothness of an arbitrary open-set boundary is assumed in the later application.

    theorem integral_extDeriv_box {n : ℕ}
        (form : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
        (hform : Differentiable ℝ form) (a b : Fin (n + 1) → ℝ) (hab : a ≤ b)
        (hint : IntegrableOn (fun x => extDeriv form x (coordinateBasis (n + 1))) (Icc a b)) :
        (∫ x in Icc a b, extDeriv form x (coordinateBasis (n + 1))) =
          ∑ i : Fin (n + 1),
            ((∫ x in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
              formFlux form i (i.insertNth (b i) x)) -
            ∫ x in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
              formFlux form i (i.insertNth (a i) x)) := by
    …

    Mentions: OAI.EilenbergGanea.coordinateBasis, OAI.EilenbergGanea.formFlux

17. theorem OAI.EilenbergGanea.extDeriv_topForm_eq_zero line 368

    Source documentation

    Every top-degree differential form on Euclidean n-space is closed.

    theorem extDeriv_topForm_eq_zero {n : ℕ}
        (φ : (Fin n → ℝ) → (Fin n → ℝ) [⋀^Fin n]→L[ℝ] ℝ) (x : Fin n → ℝ) :
        extDeriv φ x = 0 := by
    …

18. theorem OAI.EilenbergGanea.extDeriv_pullback_topForm_eq_zero line 378

    Source documentation

    The pullback of a top form by a C² map is closed (the Piola identity).

    theorem extDeriv_pullback_topForm_eq_zero {n : ℕ} {E : Type*}
        [NormedAddCommGroup E] [NormedSpace ℝ E]
        (φ : (Fin n → ℝ) → (Fin n → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
        (hφ : Differentiable ℝ φ) (F : E → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F) (x : E) :
        extDeriv (fun y => (φ (F y)).compContinuousLinearMap (fderiv ℝ F y)) x = 0 := by
    …

19. theorem OAI.EilenbergGanea.closedForm_boundary_box line 389

    Source documentation

    A closed form has total signed flux zero across the faces of a box.

    theorem closedForm_boundary_box {n : ℕ}
        (form : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
        (hform : Differentiable ℝ form) (hclosed : ∀ x, extDeriv form x = 0)
        (a b : Fin (n + 1) → ℝ) (hab : a ≤ b) :
        (∑ i : Fin (n + 1),
            ((∫ x in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
              formFlux form i (i.insertNth (b i) x)) -
            ∫ x in Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
              formFlux form i (i.insertNth (a i) x))) = 0 := by
    …

    Mentions: OAI.EilenbergGanea.formFlux

20. theorem OAI.EilenbergGanea.closedForm_opposite_faces line 405

    Source documentation

    The coefficient integrals on two opposing faces of a box agree for a closed form whose flux on all other faces is zero. This is the analytic homotopy-invariance step with the sides outside the support of the form.

    theorem closedForm_opposite_faces {n : ℕ}
        (form : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
        (hform : Differentiable ℝ form) (hclosed : ∀ x, extDeriv form x = 0)
        (a b : Fin (n + 1) → ℝ) (hab : a ≤ b) (k : Fin (n + 1))
        (hside : ∀ i, i ≠ k → ∀ x ∈ Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
          formFlux form i (i.insertNth (b i) x) = 0 ∧
          formFlux form i (i.insertNth (a i) x) = 0) :
        (∫ x in Icc (a ∘ k.succAbove) (b ∘ k.succAbove),
          formFlux form k (k.insertNth (b k) x)) =
        ∫ x in Icc (a ∘ k.succAbove) (b ∘ k.succAbove),
          formFlux form k (k.insertNth (a k) x) := by
    …

    Mentions: OAI.EilenbergGanea.formFlux

21. def OAI.EilenbergGanea.coordinateVolumeForm line 434

    Source documentation

    Determinant form with the standard coordinate orientation.

    def coordinateVolumeForm (n : ℕ) : (Fin n → ℝ) [⋀^Fin n]→L[ℝ] ℝ :=
    …

22. theorem OAI.EilenbergGanea.differentiable_pullback_topForm line 438

    Source documentation

    Smooth pullbacks of a top form are differentiable.

    theorem differentiable_pullback_topForm {n : ℕ} {E : Type*}
        [NormedAddCommGroup E] [NormedSpace ℝ E]
        (φ : (Fin n → ℝ) → (Fin n → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
        (hφ : Differentiable ℝ φ) (F : E → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F) :
        Differentiable ℝ (fun y => (φ (F y)).compContinuousLinearMap (fderiv ℝ F y)) := by
    …

23. theorem OAI.EilenbergGanea.indicator_eventuallyEq_or_zero line 451

    Source documentation

    Restricting a field to an open set whose boundary avoids its topological support is locally either the original field or zero.

    theorem indicator_eventuallyEq_or_zero {X A : Type*} [TopologicalSpace X] [Zero A]
        (U : Set X) (hU : IsOpen U) (f : X → A)
        (hb : Disjoint (frontier U) (tsupport f)) (x : X) :
        U.indicator f =ᶠ[nhds x] f ∨ U.indicator f =ᶠ[nhds x] fun _ => 0 := by
    …

24. theorem OAI.EilenbergGanea.localized_closedForm line 473

    Source documentation

    Excision at the differential-form level: cutting off at an arbitrary isolating open-set boundary preserves differentiability and closedness.

    theorem localized_closedForm {n : ℕ} {E : Type*}
        [NormedAddCommGroup E] [NormedSpace ℝ E]
        (form : E → E [⋀^Fin n]→L[ℝ] ℝ) (hform : Differentiable ℝ form)
        (hclosed : ∀ x, extDeriv form x = 0) (U : Set E) (hU : IsOpen U)
        (hb : Disjoint (frontier U) (tsupport form)) :
        Differentiable ℝ (U.indicator form) ∧ ∀ x, extDeriv (U.indicator form) x = 0 := by
    …

25. theorem OAI.EilenbergGanea.pullback_topForm_opposite_faces line 493

    Source documentation

    Homotopy-invariant integrals of a pulled-back target top form, with no unproved mapping-degree primitive.

    theorem pullback_topForm_opposite_faces {n : ℕ}
        (φ : (Fin n → ℝ) → (Fin n → ℝ) [⋀^Fin n]→L[ℝ] ℝ)
        (hφ : Differentiable ℝ φ) (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ))
        (hF : ContDiff ℝ 2 F) (a b : Fin (n + 1) → ℝ) (hab : a ≤ b)
        (k : Fin (n + 1))
        (hside : ∀ i, i ≠ k → ∀ x ∈ Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
          φ (F (i.insertNth (b i) x)) = 0 ∧ φ (F (i.insertNth (a i) x)) = 0) :
        (∫ x in Icc (a ∘ k.succAbove) (b ∘ k.succAbove),
          formFlux (fun y => (φ (F y)).compContinuousLinearMap (fderiv ℝ F y))
            k (k.insertNth (b k) x)) =
        ∫ x in Icc (a ∘ k.succAbove) (b ∘ k.succAbove),
          formFlux (fun y => (φ (F y)).compContinuousLinearMap (fderiv ℝ F y))
    …

    Mentions: OAI.EilenbergGanea.formFlux

26. theorem OAI.EilenbergGanea.coordinateVolumeForm_linear line 515

    Source documentation

    Evaluation of the standard volume form is the ordinary linear determinant.

    theorem coordinateVolumeForm_linear {n : ℕ}
        (L : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ)) :
        coordinateVolumeForm n (fun i => L (coordinateBasis n i)) = L.det := by
    …

    Mentions: OAI.EilenbergGanea.coordinateVolumeForm, OAI.EilenbergGanea.coordinateBasis

27. theorem OAI.EilenbergGanea.formFlux_pullback_first_face line 527

    Source documentation

    At a temporal face, the pullback coefficient is precisely the signed Jacobian density of the corresponding slice.

    theorem formFlux_pullback_first_face {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ))
        (t : ℝ) (x : Fin n → ℝ) (hF : DifferentiableAt ℝ F (Fin.cons t x)) :
        formFlux (fun y => ((ρ (F y)) • coordinateVolumeForm n).compContinuousLinearMap
          (fderiv ℝ F y)) 0 (Fin.cons t x) =
          (fderiv ℝ (fun z => F (Fin.cons t z)) x).det * ρ (F (Fin.cons t x)) := by
    …

    Mentions: OAI.EilenbergGanea.formFlux, OAI.EilenbergGanea.coordinateVolumeForm

28. theorem OAI.EilenbergGanea.jacobian_integral_homotopy_box line 556

    Source documentation

    Smooth homotopy invariance of the Jacobian integral against a target bump whose pullback vanishes on the spatial sides of a containing box.

    theorem jacobian_integral_homotopy_box {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) (a b : Fin n → ℝ) (hab : a ≤ b)
        (hside : ∀ i : Fin (n + 1), i ≠ 0 →
          ∀ x ∈ Icc ((Fin.cons t₀ a : Fin (n + 1) → ℝ) ∘ i.succAbove)
            ((Fin.cons t₁ b : Fin (n + 1) → ℝ) ∘ i.succAbove),
          ρ (F (i.insertNth ((Fin.cons t₁ b : Fin (n + 1) → ℝ) i) x)) = 0 ∧
          ρ (F (i.insertNth ((Fin.cons t₀ a : Fin (n + 1) → ℝ) i) x)) = 0) :
        (∫ x in Icc a b, (fderiv ℝ (fun z => F (Fin.cons t₁ z)) x).det *
          ρ (F (Fin.cons t₁ x))) =
        ∫ x in Icc a b, (fderiv ℝ (fun z => F (Fin.cons t₀ z)) x).det *
    …

29. theorem OAI.EilenbergGanea.tsupport_pullback_density_subset line 588

    Source documentation

    The support of a pulled-back density lies above the support of the target bump. This provides the needed collar at an arbitrary isolating boundary.

    theorem tsupport_pullback_density_subset {n : ℕ} {E : Type*}
        [NormedAddCommGroup E] [NormedSpace ℝ E]
        (ρ : (Fin n → ℝ) → ℝ) (F : E → (Fin n → ℝ)) (hF : Continuous F) :
        tsupport (fun y => ((ρ (F y)) • coordinateVolumeForm n).compContinuousLinearMap
          (fderiv ℝ F y)) ⊆ F ⁻¹' tsupport ρ := by
    …

    Mentions: OAI.EilenbergGanea.coordinateVolumeForm

30. theorem OAI.EilenbergGanea.jacobian_integral_homotopy_localized_box line 602

    Source documentation

    Localized homotopy invariance on an arbitrary open spatial set. The boundary collar is expressed by avoidance of the target bump, not by a smooth boundary assumption. The spatial box is only an integration device.

    theorem jacobian_integral_homotopy_localized_box {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (U : Set (Fin n → ℝ)) (hU : IsOpen U)
        (hboundary : ∀ y : Fin (n + 1) → ℝ,
          (fun i => y i.succ) ∈ frontier U → F y ∉ tsupport ρ)
        (t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) (a b : Fin n → ℝ) (hab : a ≤ b)
        (hbox : U ⊆ Icc a b)
        (hside : ∀ i : Fin (n + 1), i ≠ 0 →
          ∀ x ∈ Icc ((Fin.cons t₀ a : Fin (n + 1) → ℝ) ∘ i.succAbove)
            ((Fin.cons t₁ b : Fin (n + 1) → ℝ) ∘ i.succAbove),
          (fun j : Fin n => (i.insertNth ((Fin.cons t₁ b : Fin (n + 1) → ℝ) i) x :
    …

31. theorem OAI.EilenbergGanea.jacobian_integral_homotopy_localized line 669

    Source documentation

    Homotopy invariance on a bounded open set, without selecting a box or requiring any shape or smoothness of its boundary.

    theorem jacobian_integral_homotopy_localized {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (U : Set (Fin n → ℝ)) (hU : IsOpen U) (hUb : Bornology.IsBounded U)
        (hboundary : ∀ y : Fin (n + 1) → ℝ,
          (fun i => y i.succ) ∈ frontier U → F y ∉ tsupport ρ)
        (t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) :
        (∫ x in U, (fderiv ℝ (fun z => F (Fin.cons t₁ z)) x).det *
          ρ (F (Fin.cons t₁ x))) =
        ∫ x in U, (fderiv ℝ (fun z => F (Fin.cons t₀ z)) x).det *
          ρ (F (Fin.cons t₀ x)) := by
    …

32. theorem OAI.EilenbergGanea.jacobian_integral_homotopy_localized_interval line 709

    Source documentation

    Only boundary avoidance during the given interval is needed. Smooth saturation of the time coordinate turns it into the global collar hypothesis of the preceding Stokes argument, with the endpoints unchanged.

    theorem jacobian_integral_homotopy_localized_interval {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (U : Set (Fin n → ℝ)) (hU : IsOpen U) (hUb : Bornology.IsBounded U)
        (hboundary : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x ∈ frontier U,
          F (Fin.cons t x) ∉ tsupport ρ) :
        (∫ x in U, (fderiv ℝ (fun z => F (Fin.cons 1 z)) x).det *
          ρ (F (Fin.cons 1 x))) =
        ∫ x in U, (fderiv ℝ (fun z => F (Fin.cons 0 z)) x).det *
          ρ (F (Fin.cons 0 x)) := by
    …

33. theorem OAI.EilenbergGanea.regular_count_persists line 744

    Source documentation

    A nonzero signed regular count cannot disappear under a smooth homotopy whose boundary avoids the target. All analytic degree ingredients are proved above; in particular this is not an assumed Brouwer-degree interface.

    theorem regular_count_persists {n : ℕ}
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (y : Fin n → ℝ) (U : Set (Fin n → ℝ)) (hU : IsOpen U)
        (hc : IsCompact (closure U))
        (hb : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x ∈ frontier U, F (Fin.cons t x) ≠ y)
        (s : Finset (Fin n → ℝ))
        (hs : ∀ x, x ∈ s ↔ x ∈ U ∧ F (Fin.cons 0 x) = y)
        (hd : ∀ x ∈ s, (fderiv ℝ (fun z => F (Fin.cons 0 z)) x).det ≠ 0)
        (hcount : (∑ x ∈ s, (if 0 < (fderiv ℝ (fun z => F (Fin.cons 0 z)) x).det
          then 1 else -1 : ℝ)) ≠ 0) :
        ∃ x ∈ U, F (Fin.cons 1 x) = y := by
    …

34. theorem OAI.EilenbergGanea.regular_count_persists_finiteDimensional line 819

    Source documentation

    The analytic nonzero-count theorem is independent of a choice of linear coordinates. This form applies directly to finite products of quaternions.

    theorem regular_count_persists_finiteDimensional
        (F : ℝ × E → E) (hF : ContDiff ℝ 2 F)
        (y : E) (U : Set E) (hU : IsOpen U) (hc : IsCompact (closure U))
        (hb : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x ∈ frontier U, F (t, x) ≠ y)
        (s : Finset E) (hs : ∀ x, x ∈ s ↔ x ∈ U ∧ F (0, x) = y)
        (hd : ∀ x ∈ s, (fderiv ℝ (fun z => F (0, z)) x).det ≠ 0)
        (hcount : (∑ x ∈ s, (if 0 < (fderiv ℝ (fun z => F (0, z)) x).det
          then 1 else -1 : ℝ)) ≠ 0) : ∃ x ∈ U, F (1, x) = y := by
    …

35. theorem OAI.EilenbergGanea.regular_approximation_persists line 901

    Source documentation

    A regular perturbation at time zero can be propagated along an arbitrary boundary-root-free smooth homotopy. The perturbation need not be equivariant away from the initial time.

    theorem regular_approximation_persists
        {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
        (F : ℝ × E → E) (hF : ContDiff ℝ 2 F)
        (U : Set E) (hU : IsOpen U) (hc : IsCompact (closure U))
        (hb : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x ∈ frontier U, F (t, x) ≠ 0)
        (happrox : ∀ ε : ℝ, 0 < ε → ∃ g : E → E, ContDiff ℝ ∞ g ∧
          (∀ x ∈ closure U, ‖g x - F (0, x)‖ < ε) ∧
          ∃ s : Finset E, (∀ x, x ∈ s ↔ x ∈ closure U ∧ g x = 0) ∧
            (∀ x ∈ s, (fderiv ℝ g x).det ≠ 0) ∧
            (∑ x ∈ s, (if 0 < (fderiv ℝ g x).det then 1 else -1 : ℝ)) ≠ 0) :
        ∃ x ∈ U, F (1, x) = 0 := by
    …

36. theorem OAI.EilenbergGanea.localized_word_root_persists line 962

    Source documentation

    Localized nonsingular-exponent word-map roots cannot disappear under a boundary-root-free smooth homotopy, even though the initial word map can have singular roots.

    theorem localized_word_root_persists {m : ℕ}
        (w : Fin m → FreeGroup (Fin m)) (hB : (exponentMatrix w).det ≠ 0)
        (F : ℝ × ((Fin m → ℂ) × (Fin m → ℂ)) → ((Fin m → ℂ) × (Fin m → ℂ)))
        (hF : ContDiff ℝ 2 F) (hF0 : ∀ q, F (0, q) = splitWordMap w q)
        (U : Set ((Fin m → ℂ) × (Fin m → ℂ))) (hU : IsOpen U)
        (hc : IsCompact (closure U))
        (hUi : ∀ z : ℂ, ‖z‖ = 1 → ∀ q ∈ closure U, (q.1, z • q.2) ∈ closure U)
        (h1 : (1, 0) ∈ U)
        (hb : ∀ t ∈ Icc (0 : ℝ) 1, ∀ x ∈ frontier U, F (t, x) ≠ 0) :
        ∃ x ∈ U, F (1, x) = 0 := by
    …

    Mentions: OAI.EilenbergGanea.exponentMatrix, OAI.EilenbergGanea.splitWordMap

37. theorem OAI.EilenbergGanea.jacobian_integral_moving_box line 984

    Source documentation

    Stokes localization in an arbitrary open subset of time times space. The two slices may be different; no regularity of the moving boundary is used.

    theorem jacobian_integral_moving_box {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (C : Set (Fin (n + 1) → ℝ)) (hC : IsOpen C)
        (hboundary : ∀ y ∈ frontier C, F y ∉ tsupport ρ)
        (t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) (a b : Fin n → ℝ) (hab : a ≤ b)
        (hbox : ∀ t, {x | (Fin.cons t x : Fin (n + 1) → ℝ) ∈ C} ⊆ Icc a b)
        (hside : ∀ i : Fin (n + 1), i ≠ 0 →
          ∀ x ∈ Icc ((Fin.cons t₀ a : Fin (n + 1) → ℝ) ∘ i.succAbove)
            ((Fin.cons t₁ b : Fin (n + 1) → ℝ) ∘ i.succAbove),
          i.insertNth ((Fin.cons t₁ b : Fin (n + 1) → ℝ) i) x ∉ C ∧
          i.insertNth ((Fin.cons t₀ a : Fin (n + 1) → ℝ) i) x ∉ C) :
    …

38. theorem OAI.EilenbergGanea.jacobian_integral_moving line 1049

    Source documentation

    Box-free moving-domain Stokes, with arbitrary open moving slices contained in one bounded spatial set.

    theorem jacobian_integral_moving {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (C : Set (Fin (n + 1) → ℝ)) (hC : IsOpen C)
        (hboundary : ∀ y ∈ frontier C, F y ∉ tsupport ρ)
        (hCb : Bornology.IsBounded {x : Fin n → ℝ | ∃ t : ℝ, Fin.cons t x ∈ C})
        (t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) :
        (∫ x in {x | (Fin.cons t₁ x : Fin (n + 1) → ℝ) ∈ C},
          (fderiv ℝ (fun z => F (Fin.cons t₁ z)) x).det * ρ (F (Fin.cons t₁ x))) =
        ∫ x in {x | (Fin.cons t₀ x : Fin (n + 1) → ℝ) ∈ C},
          (fderiv ℝ (fun z => F (Fin.cons t₀ z)) x).det * ρ (F (Fin.cons t₀ x)) := by
    …

39. theorem OAI.EilenbergGanea.jacobian_integral_moving_interval line 1090

    Source documentation

    Smooth time saturation reduces the collar hypothesis to the actual time interval even for moving open domains.

    theorem jacobian_integral_moving_interval {n : ℕ}
        (ρ : (Fin n → ℝ) → ℝ) (hρ : Differentiable ℝ ρ)
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (C : Set (Fin (n + 1) → ℝ)) (hC : IsOpen C)
        (hboundary : ∀ y ∈ frontier C, y 0 ∈ Icc (0 : ℝ) 1 → F y ∉ tsupport ρ)
        (hCb : Bornology.IsBounded {x : Fin n → ℝ | ∃ t ∈ Icc (0 : ℝ) 1, Fin.cons t x ∈ C}) :
        (∫ x in {x | (Fin.cons 1 x : Fin (n + 1) → ℝ) ∈ C},
          (fderiv ℝ (fun z => F (Fin.cons 1 z)) x).det * ρ (F (Fin.cons 1 x))) =
        ∫ x in {x | (Fin.cons 0 x : Fin (n + 1) → ℝ) ∈ C},
          (fderiv ℝ (fun z => F (Fin.cons 0 z)) x).det * ρ (F (Fin.cons 0 x)) := by
    …

40. theorem OAI.EilenbergGanea.regular_count_persists_moving line 1130

    Source documentation

    A nonzero signed count survives an arbitrary moving open set. The compact boundary slab hypothesis is satisfied by the fixed annulus in the quaternion application; no boundary triangulation or regular-value hypothesis is used along the homotopy.

    theorem regular_count_persists_moving {n : ℕ}
        (F : (Fin (n + 1) → ℝ) → (Fin n → ℝ)) (hF : ContDiff ℝ 2 F)
        (y : Fin n → ℝ) (C : Set (Fin (n + 1) → ℝ)) (hC : IsOpen C)
        (hc₀ : IsCompact (closure {x | (Fin.cons 0 x : Fin (n + 1) → ℝ) ∈ C}))
        (hc₁ : IsCompact (closure {x | (Fin.cons 1 x : Fin (n + 1) → ℝ) ∈ C}))
        (hcB : IsCompact {q | q ∈ frontier C ∧ q 0 ∈ Icc (0 : ℝ) 1})
        (hCb : Bornology.IsBounded {x : Fin n → ℝ | ∃ t ∈ Icc (0 : ℝ) 1, Fin.cons t x ∈ C})
        (hb : ∀ q ∈ frontier C, q 0 ∈ Icc (0 : ℝ) 1 → F q ≠ y)
        (s : Finset (Fin n → ℝ))
        (hs : ∀ x, x ∈ s ↔ Fin.cons 0 x ∈ C ∧ F (Fin.cons 0 x) = y)
        (hd : ∀ x ∈ s, (fderiv ℝ (fun z => F (Fin.cons 0 z)) x).det ≠ 0)
        (hcount : (∑ x ∈ s, (if 0 < (fderiv ℝ (fun z => F (Fin.cons 0 z)) x).det
    …

41. theorem OAI.EilenbergGanea.regular_count_persists_moving_finiteDimensional line 1200

    Source documentation

    Coordinate-free moving-domain nonzero-count persistence.

    theorem regular_count_persists_moving_finiteDimensional
        (F : ℝ × E → E) (hF : ContDiff ℝ 2 F) (y : E)
        (C : Set (ℝ × E)) (hC : IsOpen C)
        (hc₀ : IsCompact (closure {x | (0, x) ∈ C}))
        (hc₁ : IsCompact (closure {x | (1, x) ∈ C}))
        (hcB : IsCompact {q : ℝ × E | q ∈ frontier C ∧ q.1 ∈ Icc (0 : ℝ) 1})
        (hCb : Bornology.IsBounded {x : E | ∃ t ∈ Icc (0 : ℝ) 1, (t, x) ∈ C})
        (hb : ∀ q ∈ frontier C, q.1 ∈ Icc (0 : ℝ) 1 → F q ≠ y)
        (s : Finset E) (hs : ∀ x, x ∈ s ↔ (0, x) ∈ C ∧ F (0, x) = y)
        (hd : ∀ x ∈ s, (fderiv ℝ (fun z => F (0, z)) x).det ≠ 0)
        (hcount : (∑ x ∈ s, (if 0 < (fderiv ℝ (fun z => F (0, z)) x).det
          then 1 else -1 : ℝ)) ≠ 0) : ∃ x, (1, x) ∈ C ∧ F (1, x) = y := by
    …

42. theorem OAI.EilenbergGanea.regular_approximation_persists_moving line 1315

    Source documentation

    Arbitrarily small regular approximations at the initial slice suffice for moving-domain continuation. Uniform closeness is requested on the spatial projection of the boundary slab, not on an assumed fixed isolating domain.

    theorem regular_approximation_persists_moving
        (F : ℝ × E → E) (hF : ContDiff ℝ 2 F)
        (C : Set (ℝ × E)) (hC : IsOpen C)
        (hc₀ : IsCompact (closure {x | (0, x) ∈ C}))
        (hc₁ : IsCompact (closure {x | (1, x) ∈ C}))
        (hcB : IsCompact {q : ℝ × E | q ∈ frontier C ∧ q.1 ∈ Icc (0 : ℝ) 1})
        (hCb : Bornology.IsBounded {x : E | ∃ t ∈ Icc (0 : ℝ) 1, (t, x) ∈ C})
        (hb : ∀ q ∈ frontier C, q.1 ∈ Icc (0 : ℝ) 1 → F q ≠ 0)
        (L : Set E) (hLB : ∀ q ∈ frontier C, q.1 ∈ Icc (0 : ℝ) 1 → q.2 ∈ L)
        (happrox : ∀ ε : ℝ, 0 < ε → ∃ g : E → E, ContDiff ℝ ∞ g ∧
          (∀ x ∈ L, ‖g x - F (0, x)‖ < ε) ∧
          ∃ s : Finset E, (∀ x, x ∈ s ↔ x ∈ closure {z | (0, z) ∈ C} ∧ g x = 0) ∧
    …

43. theorem OAI.EilenbergGanea.localized_word_root_persists_moving line 1382

    Source documentation

    Full localized word-root persistence for moving open sets. Contains the singular pure-word initial maps used in the manuscript's finite-quotient step.

    theorem localized_word_root_persists_moving {m : ℕ}
        (w : Fin m → FreeGroup (Fin m)) (hB : (exponentMatrix w).det ≠ 0)
        (F : ℝ × ((Fin m → ℂ) × (Fin m → ℂ)) → ((Fin m → ℂ) × (Fin m → ℂ)))
        (hF : ContDiff ℝ 2 F) (hF0 : ∀ q, F (0, q) = splitWordMap w q)
        (C : Set (ℝ × ((Fin m → ℂ) × (Fin m → ℂ)))) (hC : IsOpen C)
        (hc₀ : IsCompact (closure {x | (0, x) ∈ C}))
        (hc₁ : IsCompact (closure {x | (1, x) ∈ C}))
        (hcB : IsCompact {q | q ∈ frontier C ∧ q.1 ∈ Icc (0 : ℝ) 1})
        (hCb : Bornology.IsBounded {x | ∃ t ∈ Icc (0 : ℝ) 1, (t, x) ∈ C})
        (hUi : ∀ z : ℂ, ‖z‖ = 1 → ∀ q ∈ closure {x | (0, x) ∈ C},
          (q.1, z • q.2) ∈ closure {x | (0, x) ∈ C})
        (h1 : (0, (1, 0)) ∈ C)
    …

    Mentions: OAI.EilenbergGanea.exponentMatrix, OAI.EilenbergGanea.splitWordMap