OAI/GroupTheory/Kervaire/CurrentExistence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KervaireCurrentExistence.mem_range_of_integral_invariant line 44

   Source documentation

   The nonzero local degree forces a target point into the other endpoint's image. All localization is justified by compactness, smooth bumps and positivity of Haar measure.

   lemma mem_range_of_integral_invariant {f₀ f₁ : S → E} {j₀ j₁ : S → ℝ}
       (hf₀ : Continuous f₀) (hf₁ : Continuous f₁) (hj₀ : Continuous j₀)
       (y : E) (hex : ∃ x, f₀ x = y) (hpos : ∀ x, f₀ x = y → 0 < j₀ x)
       (hinv : ∀ φ : E → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ →
         (∫ x, φ (f₀ x) * j₀ x ∂μ) = ∫ x, φ (f₁ x) * j₁ x ∂μ) :
       y ∈ Set.range f₁ := by
   …

2. def OAI.KervaireIncidenceCurrent.modelMap line 90
3. lemma OAI.KervaireIncidenceCurrent.exists_incidence_of_homotopic_basis line 97
4. lemma OAI.KervaireIncidenceCurrent.skew_finrank_pos line 131
5. lemma OAI.KervaireIncidenceCurrent.exists_incidence_of_homotopic line 143