SeededInverse.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The inverse acting on already normalized individual jets

Only the additional derivative orders enter the extracted radius weight. The formula also permits a complex angular multiplier as a separate label.

theorem OAI.Falconer.MaskJetIndex.value_scaled_input line 19
def OAI.Falconer.MaskJetExpansion.seededRadiusWeight line 33
theorem OAI.Falconer.MaskJetExpansion.seededRadiusWeight_nonneg line 37
theorem OAI.Falconer.MaskJetExpansion.seededRadiusWeight_le line 42
theorem OAI.Falconer.MaskJetExpansion.inverse_seed_term_normalized line 49
theorem OAI.Falconer.MaskJetExpansion.localInverseAmplitude_seeded_jets line 83
Source documentation
Exact global expansion with every old radius normalization cancelled.
```
theorem localInverseAmplitude_seeded_jets (m j : ℕ) (k : ι → MaskJetIndex (m+3))
    (r : ι → ℝ) (hr : ∀ i, r i ≠ 0) (B : ι → X → Space (m+3) → ℂ)
    (hB : ∀ i x, ContDiff ℝ ∞ (B i x)) (x : X) (e : Sphere (m+3)) :
    let T := (seed k).inverse m j
…
```
Mentions: OAI.Falconer.MaskJetIndex, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.MaskJetExpansion.inverse
theorem OAI.Falconer.MaskJetExpansion.card_inverse_seed line 108
Source documentation
Term count is unchanged by the initial derivative orders.
```
theorem card_inverse_seed (m j : ℕ) (k : ι → MaskJetIndex (m+3)) :
    Fintype.card ((seed k).inverse m j).index =
      inverseMultiplicity (m+2) j * (1+Fintype.card ι*(m+3))^(2*j) := by
…
```
Mentions: OAI.Falconer.MaskJetIndex, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.MaskJetExpansion.inverse, OAI.Falconer.MaskJetExpansion.inverseMultiplicity
theorem OAI.Falconer.MaskJetExpansion.inverse_seed_geometryCoveredBy_unit line 117
Source documentation
The smooth coefficients are drawn from a fixed finite geometric family, independent of the number and previous orders of the masks.
```
theorem inverse_seed_geometryCoveredBy_unit (m j : ℕ) (k : ι → MaskJetIndex (m+3)) :
    ((seed k).inverse m j).GeometryCoveredBy
      ((product : MaskJetExpansion Unit (m+3) (Space (m+3))).inverse m j) :=
…
```
Mentions: OAI.Falconer.MaskJetIndex, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.MaskJetExpansion.inverse, OAI.Falconer.MaskJetExpansion.GeometryCoveredBy, OAI.Falconer.MaskJetExpansion.product, OAI.Falconer.MaskJetExpansion, OAI.Falconer.Space
theorem OAI.Falconer.MaskJetExpansion.inverse_seed_coefficient_derivatives line 123