InverseClassExpansion.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact inverse expansion in the recursive symbol class

The finite family is constructed from the actual differentiated masks. Its constants are uniform in both descriptor lists, and the output keeps the two original spatial multipliers and the remaining smoothness budget.

abbrev OAI.Falconer.DescriptorInverseIndex line 18
theorem OAI.Falconer.card_descriptorInverseIndex line 23
theorem OAI.Falconer.descriptorInverseWeight_nonneg line 35
structure OAI.Falconer.DescriptorInverseSymbols line 44
Source documentation
The exact factors delivered by the finite inverse calculation.
```
structure DescriptorInverseSymbols
    (f : DescriptorJetSymbol (m+1) KL L F D)
    (g : DescriptorJetSymbol (m+1) KR L G D) (j R : ℕ) (A B : ℝ) where
…
```
Mentions: OAI.Falconer.DescriptorJetSymbol

theorem OAI.Falconer.exists_descriptorInverseSymbols line 62

Source documentation

The constants are selected before the lists, scale, and input symbols.

theorem exists_descriptorInverseSymbols (m j R : ℕ) :
    ∃ A B : ℝ, 1 ≤ A ∧ 1 ≤ B ∧
      ∀ (KL KR L : ℕ) (F G : Finset PolicyDescriptor) (D : ℝ)
        (f : DescriptorJetSymbol (m+1) KL L F D)
        (g : DescriptorJetSymbol (m+1) KR L G D),
        1 ≤ D → R+2*j ≤ L → Nonempty (DescriptorInverseSymbols f g j R A B) := by
…

Mentions: OAI.Falconer.DescriptorJetSymbol, OAI.Falconer.DescriptorInverseSymbols

theorem OAI.Falconer.DescriptorInverseSymbols.left_restore line 82
theorem OAI.Falconer.DescriptorInverseSymbols.right_restore line 95

theorem OAI.Falconer.DescriptorInverseSymbols.expansion line 110

Source documentation

The exact finite inverse identity expressed using actual recursive symbols. Every radius loss is on a newly added derivative.

theorem expansion (T : DescriptorInverseSymbols f g j R A B)
    (hD : 0 < D) (hA : 0 < A) (hB : 0 < B)
    (Q : DyadicCube (m+3)) (ρ : Measure (Space (m+3))) (profile : ℝ → ℝ)
    (N : ℕ) (σ : ℝ) (J i : ℕ) (S : PolicyDescriptor → Finset (Sphere (m+3)))
    (Af Ag : ℝ) {U V : ℝ} (hU : 0 < U) (hV : 0 < V)
    (x y : Space (m+3)) (e : Sphere (m+3)) :
    localInverseAmplitude m
      (fun z => f.ambient Q ρ profile N σ J i S Af x z *
        g.ambient Q ρ profile N σ J i S Ag y z) j e =
      ∑ a : DescriptorInverseIndex f g j,
        ((descriptorInverseWeight f g j N σ a * (U*A) * (V*B) * Af⁻¹ * Ag⁻¹ : ℝ) : ℂ) *
          ((T.left a).value Q ρ profile N σ J i S U x e *
…

Mentions: OAI.Falconer.DescriptorInverseSymbols, OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.localInverseAmplitude, OAI.Falconer.DescriptorInverseIndex, OAI.Falconer.descriptorInverseWeight