InverseJetSymbols.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual recursive symbols produced by the inverse

The old descriptor list and spatial multiplier survive unchanged. The angular multiplier is the geometric inverse coefficient times the newly differentiated old multiplier, with a fixed normalization. The new finite smoothness budget is explicit.

theorem OAI.Falconer.MaskJetExpansion.seed_inverse_right_order line 20
def OAI.Falconer.DescriptorJetSymbol.inverseRightJets line 44
theorem OAI.Falconer.DescriptorJetSymbol.inverseRightJets_order line 52

theorem OAI.Falconer.exists_inverse_left_symbol line 85

Source documentation

The left endpoint factor of each actual inverse term belongs to the factorized class. The old multiplier needs R+2*j available derivatives.

theorem exists_inverse_left_symbol (m j R : ℕ) :
    ∃ A : ℝ, 1 ≤ A ∧ ∀ (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 →
      ∀ a : ((MaskJetExpansion.seed (descriptorInverseSeed f g)).inverse m j).index,
      ∃ u : DescriptorJetSymbol (m+1) (KL+2*j) R F D,
        u.jet = f.inverseLeftJets g j a ∧ u.spatial = f.spatial ∧
        u.angular = normalizedAngular A
          (fun z => (((MaskJetExpansion.seed (descriptorInverseSeed f g)).inverse m j).term a).coefficient z *
            ((((MaskJetExpansion.seed (descriptorInverseSeed f g)).inverse m j).term a).jet
              (.inl (.inl ()))).scaledValue D⁻¹ f.angular z) := by
…

Mentions: OAI.Falconer.DescriptorJetSymbol, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.descriptorInverseSeed, OAI.Falconer.normalizedAngular

theorem OAI.Falconer.exists_inverse_right_symbol line 123

Source documentation

The right endpoint retains its own original descriptors and spatial multiplier. Its angular factor has no geometric coefficient.

theorem exists_inverse_right_symbol (m j R : ℕ) :
    ∃ A : ℝ, 1 ≤ A ∧ ∀ (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 →
      ∀ a : ((MaskJetExpansion.seed (descriptorInverseSeed f g)).inverse m j).index,
      ∃ u : DescriptorJetSymbol (m+1) (KR+2*j) R G D,
        u.jet = f.inverseRightJets g j a ∧ u.spatial = g.spatial ∧
        u.angular = normalizedAngular A
          (((((MaskJetExpansion.seed (descriptorInverseSeed f g)).inverse m j).term a).jet
              (.inr (.inl ()))).scaledValue D⁻¹ g.angular) := by
…

Mentions: OAI.Falconer.DescriptorJetSymbol, OAI.Falconer.MaskJetExpansion.seed, OAI.Falconer.descriptorInverseSeed, OAI.Falconer.normalizedAngular