proposition: Fact sum_power_binary_lt p n f a : 0 < p <= q -> (forall i j, i < j < n -> f i < f j) -> (forall i, i < n -> a i < power p 2) -> ∑ n (fun i => a i * power (f i) r) ≲ (power p 2-1) * ∑ n (fun i => power (f i) r).
proof: Proof. Proof using Hq Hr. intros H1 H2 H3. generalize (sinc_injective _ H2); intros H4. rewrite <- sum_0n_scal_l. apply binary_le_nat_meet. rewrite meet_sum_powers; auto. 2: intros i Hi; rewrite Hr; apply Nat.lt_le_trans with (1 := H3 _ Hi), power_mono_l; lia. 2: { rewrite Hr. intros i Hi. generalize (@power_ge_1 p 2); intro. unfold lt. replace (S (power p 2 -1)) with (power p 2); try lia. apply power_mono_l; lia. } apply msum_ext; intros i Hi; f_equal. apply binary_le_nat_meet, power_2_minus_1_gt. assert (a i < power p 2); try lia. apply Nat.lt_le_trans with (1 := H3 _ Hi), power_mono_l; lia. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)