FiniteResidueIndices.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.residueIndices line 11
Source documentation
Natural indices for a finite sample space. Distinct samples remain distinct indices even when their integer-valued data agree.
```
def residueIndices (α : Type*) [Fintype α] : Finset ℕ :=
…
```
def OAI.Problem337.residueEntry line 15
Source documentation
Extend finite sample data by zero outside their canonical natural indices.
```
def residueEntry {α β : Type*} [Fintype α] [Zero β] (f : α → β) (i : ℕ) : β :=
…
```
theorem OAI.Problem337.residueIndices_card line 18
theorem OAI.Problem337.mem_residueIndices line 22
theorem OAI.Problem337.residueEntry_equivFin line 26
theorem OAI.Problem337.residueIndices_nonempty_iff line 32
Source documentation
Nonemptiness transfers without any injectivity requirement on the data.
```
@[simp] theorem residueIndices_nonempty_iff (α : Type*) [Fintype α] :
    (residueIndices α).Nonempty ↔ Nonempty α := by
…
```
Mentions: OAI.Problem337.residueIndices
theorem OAI.Problem337.forall_residueEntry_iff line 37
Source documentation
A pointwise assertion can be transported to the numeric indices.
```
theorem forall_residueEntry_iff {α β : Type*} [Fintype α] [Zero β]
    (f : α → β) (P : β → Prop) :
    (∀ i ∈ residueIndices α, P (residueEntry f i)) ↔ ∀ a, P (f a) := by
…
```
Mentions: OAI.Problem337.residueIndices, OAI.Problem337.residueEntry

theorem OAI.Problem337.sum_residueEntry line 48

Source documentation

Full finite sums preserve sample multiplicity under the natural reindexing.

theorem sum_residueEntry {α β γ : Type*} [Fintype α] [Zero β]
    [AddCommMonoid γ] (f : α → β) (g : β → γ) :
    (∑ i ∈ residueIndices α, g (residueEntry f i)) = ∑ a, g (f a) := by
…

Mentions: OAI.Problem337.residueIndices, OAI.Problem337.residueEntry

theorem OAI.Problem337.card_filter_residueEntry line 59

Source documentation

Filtering keeps repeated equal data as distinct samples.

theorem card_filter_residueEntry {α β : Type*} [Fintype α] [Zero β]
    (f : α → β) (P : β → Prop) [DecidablePred P] :
    ((residueIndices α).filter (fun i => P (residueEntry f i))).card =
      (Finset.univ.filter (fun a : α => P (f a))).card := by
…

Mentions: OAI.Problem337.residueIndices, OAI.Problem337.residueEntry

theorem OAI.Problem337.forall_residueEntry₂_iff line 68

Source documentation

The same sample is used for all components of indexed arithmetic data.

theorem forall_residueEntry₂_iff {α β γ : Type*} [Fintype α] [Zero β] [Zero γ]
    (f : α → β) (g : α → γ) (P : β → γ → Prop) :
    (∀ i ∈ residueIndices α, P (residueEntry f i) (residueEntry g i)) ↔
      ∀ a, P (f a) (g a) := by
…

Mentions: OAI.Problem337.residueIndices, OAI.Problem337.residueEntry

theorem OAI.Problem337.residueEntry_apply line 80

Source documentation

Function-valued residue or quotient data commute with evaluation.

@[simp] theorem residueEntry_apply {α β γ : Type*} [Fintype α] [Zero γ]
    (f : α → β → γ) (i : ℕ) (b : β) :
    residueEntry f i b = residueEntry (fun a => f a b) i := by
…

Mentions: OAI.Problem337.residueEntry

theorem OAI.Problem337.normalized_sum_residueEntry line 88

Source documentation

Reindexing does not change the normalized complex Fourier sum, even when sample data have repeated values or the sample space is empty.

theorem normalized_sum_residueEntry {α β : Type*} [Fintype α] [Zero β]
    (f : α → β) (phase : β → ℂ) :
    ((residueIndices α).card : ℂ)⁻¹ *
        (∑ i ∈ residueIndices α, phase (residueEntry f i)) =
      (Fintype.card α : ℂ)⁻¹ * ∑ a, phase (f a) := by
…

Mentions: OAI.Problem337.residueIndices, OAI.Problem337.residueEntry