DescriptorSeededInverse.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The seeded inverse identity for actual recursive amplitudes

Both endpoint symbols use their original ambient masks. Spatial factors are pulled out exactly, and only newly added derivatives pay radius powers.

def OAI.Falconer.descriptorInverseRadius line 18
def OAI.Falconer.descriptorInverseWeight line 23
theorem OAI.Falconer.descriptorInverseRadius_pos line 30
theorem OAI.Falconer.descriptorInverseWeight_le line 39

theorem OAI.Falconer.descriptor_seeded_inverse line 59

Source documentation

Exact inverse formula before replacing the endpoint factors by their normalized output symbols.

theorem descriptor_seeded_inverse
    (f : DescriptorJetSymbol (m+1) KL L F D) (g : DescriptorJetSymbol (m+1) KR L G D)
    (hD : 0 < D) (j : ℕ) (Q : DyadicCube (m+3)) (ρ : Measure (Space (m+3)))
    (profile : ℝ → ℝ) (N : ℕ) (σ : ℝ) (J i : ℕ)
    (S : PolicyDescriptor → Finset (Sphere (m+3))) (Af Ag : ℝ)
    (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 =
      (f.spatial x*(Af⁻¹ : ℝ))*(g.spatial y*(Ag⁻¹ : ℝ))*
        ((descriptorInverseSeparation f g j Q ρ profile N σ J i S).scaleTerms
          (fun a => (descriptorInverseWeight f g j N σ a : ℂ))).value x y e := by
…

Mentions: OAI.Falconer.DescriptorJetSymbol, OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.Sphere, OAI.Falconer.localInverseAmplitude, OAI.Falconer.descriptorInverseSeparation, OAI.Falconer.descriptorInverseWeight