OAI/MeasureTheory/Falconer/Fourier/InverseMaskJets.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

The actual inverse as finite products of individual mask jets

The construction follows the already proved safe-chart inverse recursion. All mask occurrences survive in every term, and the total order charged to them is at most twice the inverse index.

  1. structure OAI.Falconer.MaskJetExpansion line 16
  2. def OAI.Falconer.MaskJetExpansion.value line 29
  3. def OAI.Falconer.MaskJetExpansion.HasOrder line 33
  4. theorem OAI.Falconer.MaskJetExpansion.value_contDiff line 36
  5. def OAI.Falconer.MaskJetExpansion.product line 41
  6. theorem OAI.Falconer.MaskJetExpansion.product_value line 46
  7. theorem OAI.Falconer.MaskJetExpansion.product_hasOrder line 51
  8. def OAI.Falconer.MaskJetExpansion.mulFixed line 55
  9. theorem OAI.Falconer.MaskJetExpansion.mulFixed_value line 59
  10. def OAI.Falconer.MaskJetExpansion.pullback line 66
  11. theorem OAI.Falconer.MaskJetExpansion.pullback_value line 70
  12. def OAI.Falconer.MaskJetExpansion.sum line 74
  13. theorem OAI.Falconer.MaskJetExpansion.sum_value line 78
  14. def OAI.Falconer.MaskJetExpansion.derivative line 83
  15. theorem OAI.Falconer.MaskJetExpansion.derivative_value line 88
  16. theorem OAI.Falconer.MaskJetExpansion.HasOrder.mulFixed line 101
  17. theorem OAI.Falconer.MaskJetExpansion.HasOrder.pullback line 105
  18. theorem OAI.Falconer.MaskJetExpansion.sum_hasOrder line 109
  19. theorem OAI.Falconer.MaskJetExpansion.HasOrder.derivative line 113
  20. def OAI.Falconer.MaskJetExpansion.laplacian line 117
  21. theorem OAI.Falconer.MaskJetExpansion.laplacian_value line 121
  22. theorem OAI.Falconer.MaskJetExpansion.HasOrder.laplacian line 140
  23. def OAI.Falconer.MaskJetExpansion.iteratedLaplacian line 144
  24. theorem OAI.Falconer.MaskJetExpansion.iteratedLaplacian_value line 148
  25. theorem OAI.Falconer.MaskJetExpansion.HasOrder.iteratedLaplacian line 161
  26. def OAI.Falconer.MaskJetExpansion.stationaryJet line 171
  27. theorem OAI.Falconer.MaskJetExpansion.stationaryJet_value line 180
  28. theorem OAI.Falconer.MaskJetExpansion.HasOrder.stationaryJet line 192
  29. def OAI.Falconer.MaskJetExpansion.inverse line 201
  30. theorem OAI.Falconer.MaskJetExpansion.inverse_value line 210
  31. theorem OAI.Falconer.MaskJetExpansion.HasOrder.inverse line 230
  32. def OAI.Falconer.MaskJetExpansion.HasPointAt line 248

    Source documentation

    Every individual mask jet in the expansion is evaluated at the same point.

    def HasPointAt (S : MaskJetExpansion ι d E) (z : E) (p : Space d) : Prop :=
…

    Mentions: OAI.Falconer.MaskJetExpansion, OAI.Falconer.Space

  33. theorem OAI.Falconer.MaskJetExpansion.product_hasPointAt line 252
  34. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.mulFixed line 256
  35. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.pullback line 261
  36. theorem OAI.Falconer.MaskJetExpansion.sum_hasPointAt line 266
  37. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.derivative line 270
  38. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.laplacian line 277
  39. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.iteratedLaplacian line 282
  40. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.stationaryJet line 292
  41. theorem OAI.Falconer.MaskJetExpansion.HasPointAt.inverse line 310
  42. theorem OAI.Falconer.MaskJetExpansion.localInverseAmplitude_product_jets line 331

    Source documentation

    The actual inverse coefficient has a finite expansion into individual mask jets, with at most 2*j derivatives in total. On the fixed patch all those jets are evaluated at the original sphere point.

    theorem localInverseAmplitude_product_jets [DecidableEq ι] (m j : ℕ) :
    ∃ S : MaskJetExpansion ι (m+3) (Space (m+3)), S.HasOrder (2*j) ∧
      (∀ (B : ι → X → Space (m+3) → ℂ),
        (∀ i x, ContDiff ℝ ∞ (B i x)) → ∀ x e,
        S.value B x e = localInverseAmplitude m (fun z => ∏ i, B i x z) j e) ∧
      (∀ e : Sphere (m+3),
        ‖(e : Space (m+3))-(gnomonicChart (0 : Space (m+2)) : Space (m+3))‖ ≤ 1/2 →
        S.HasPointAt e e) := by
…

    Mentions: OAI.Falconer.MaskJetExpansion, OAI.Falconer.Space, OAI.Falconer.localInverseAmplitude, OAI.Falconer.Sphere, OAI.Falconer.gnomonicChart