SourceSelectorConcentrationCenteredFamily.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The centered main part has one weighted physical exception for all tops and both required jets. Three monotone cutoffs produce only a fixed loss, absorbed in the polynomial threshold.

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozen_centered_rawInterval_eq line 19

Source documentation

Exact centered interval identity, including cutoff boundaries.

theorem frozen_centered_rawInterval_eq
    (P : SourceLatticePacket N κ ι)
    (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
    (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
    (t : ℝ) (d : Fin N → ℝ) (hd : ∀ j, 0 ≤ d j)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
    (i : Fin 3) (lower upper : ℕ) (x y : ℝ) :
    (P.withProfile alt hAlt).rawInterval
        ((P.frozenProfile c hc).physicalCenteredCoefficient t t d v g) i lower upper x y =
      (P.withProfile alt hAlt).rawInterval
…

Mentions: OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SourceLatticePacket.rawInterval, OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredCoefficient

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozen_physical_rawInterval_eq_reference line 69

Source documentation

Each one-sided physical coefficient is the same original reference integral after the measure-preserving shear.

theorem frozen_physical_rawInterval_eq_reference
    (P : SourceLatticePacket N κ ι)
    (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
    (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
    (t : ℝ) (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (i : Fin 3) (lower upper : ℕ) (x y : ℝ) :
    (P.withProfile alt hAlt).rawInterval
        ((P.frozenProfile c hc).physicalCoefficient t d v g) i lower upper x y =
      (P.withProfile alt hAlt).rawInterval
        ((P.frozenProfile c hc).family.mainCoefficient d
          (fun z => v (sourceReferenceToPhysical t z))
…

def OAI.LipschitzHilbert.SourceLatticePacket.centeredPhaseCutoff line 90
Also declared: OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedConcentrationCentered.lean:18 (same declaration text).
def OAI.LipschitzHilbert.SourceLatticePacket.centeredPhaseField line 93
Also declared: OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedConcentrationCentered.lean:21 (same declaration text).
theorem OAI.LipschitzHilbert.SourceLatticePacket.source_frozen_centered_family_concentration line 97